Add iset.mm notes about ring irreducibility, ring primes, and group a…

…nd ring homomorphism (metamath#4649)

* Add irreducibility theorems to mmil.html

This is isirred , isnirred , isirred2 , opprirred , irredn0 ,
irredcl , irrednu , irredn1 , irredrmul , irredlmul ,
irredmul , irredneg , and irrednegb .

* Add df-rprm to mmil.html

* Add RingHom and RingIso to iset.mm

This is the syntax , df-rnghom , and df-rngiso .  Copied without change
from set.mm.

* add df-ric to mmil.html

* Add dfrhm2 to mmil.html

* Add group homomorphism to mmil.html

This is df-ghm , isghm , isghm3 , ghmgrp1 , ghmgrp2 , ghmf , ghmlin ,
ghmid , ghminv , ghmsub , isghmd , and ghmmhm (probably other GrpHom
theorems could be listed too, I didn't try to find them all).

iset.mm

@@ -151059,6 +151059,38 @@ the additive structure must be abelian (see ~ ringcom ), care must be
   $}
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Ring homomorphisms
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $c RingHom $. $( Ring homomorphism $)
+  $c RingIso $. $( Ring isomorphism $)
+
+  $( Extend class notation with the ring homomorphisms. $)
+  crh $a class RingHom $.
+
+  $( Extend class notation with the ring isomorphisms. $)
+  crs $a class RingIso $.
+
+  ${
+    $d r s v w f x y $.
+    $( Define the set of ring homomorphisms from ` r ` to ` s ` .  (Contributed
+       by Stefan O'Rear, 7-Mar-2015.) $)
+    df-rnghom $a |- RingHom = ( r e. Ring , s e. Ring |->
+      [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_
+   { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v
+   ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\
+     ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } ) $.
+
+    $( Define the set of ring isomorphisms from ` r ` to ` s ` .  (Contributed
+       by Stefan O'Rear, 7-Mar-2015.) $)
+    df-rngiso $a |- RingIso = ( r e. _V , s e. _V |->
+      { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } ) $.
+  $}
+
+
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
   The complex numbers as an algebraic extensible structure
@@ -168334,6 +168366,12 @@ Norman Megill (2007) section 1.1.3.  Megill then states, "A number of
 htmldef "/r" as "/<SUB>r</SUB>";
   althtmldef "/r" as "/<SUB>r</SUB>";
   latexdef "/r" as "/_r";
+htmldef "RingHom" as " RingHom ";
+  althtmldef "RingHom" as " RingHom ";
+  latexdef "RingHom" as " \mathrm{RingHom} ";
+htmldef "RingIso" as " RingIso ";
+  althtmldef "RingIso" as " RingIso ";
+  latexdef "RingIso" as " \mathrm{RingIso} ";
 htmldef "numer" as "numer";
   althtmldef "numer" as "numer";
   latexdef "numer" as "\mathrm{numer}";

mmil.raw.html

@@ -10686,6 +10686,14 @@
   <td>the set.mm proof uses pwspjmhm and pwsmnd</td>
 </tr>
 
+<tr>
+  <td>df-ghm , isghm , isghm3 , ghmgrp1 , ghmgrp2 , ghmf , ghmlin ,
+  ghmid , ghminv , ghmsub , isghmd , ghmmhm</td>
+  <td><i>none</i></td>
+  <td>should be feasible in a way similar to what we did for
+  ~ df-mhm and related theorems</td>
+</tr>
+
 <tr>
   <td>setsplusg</td>
   <td>~ setsslnid</td>
@@ -10989,6 +10997,40 @@
   <td>adds ` K e. Ring ` and ` L e. Ring ` conditions</td>
 </tr>
 
+<tr>
+  <td>isirred , isnirred , isirred2 , opprirred , irredn0 ,
+  irredcl , irrednu , irredn1 , irredrmul , irredlmul ,
+  irredmul , irredneg , irrednegb</td>
+  <td><i>none</i></td>
+  <td>although there might be some way to express the
+  concept of irreducibility, it would require a close
+  look at how negation is being used throughout this
+  section</td>
+</tr>
+
+<tr>
+  <td>df-rprm</td>
+  <td><i>none</i></td>
+  <td>compare with ~ isprm6 and consider questions like whether
+  properties like decidable equality are needed to make
+  this definition function as intended</td>
+</tr>
+
+<tr>
+  <td>dfrhm2</td>
+  <td><i>none</i></td>
+  <td>presumably not hard once isghm3 is available</td>
+</tr>
+
+<tr>
+  <td>df-ric and all ring isomorphism relation theorems</td>
+  <td><i>none</i></td>
+  <td>This should be definable in some way but
+  it isn't clear whether the set.mm definition would work
+  or whether the definition needs to be more like brric2 or
+  the ` E. f f e. ( R RingIso S ) ` portion thereof.</td>
+</tr>
+
 <tr>
   <td>df-drng</td>
   <td><i>none</i></td>