Intuitionize the rest of the section "Definition and basic properties…

… of unital rings" (#4545)

* copy ringlz and ringrz from set.mm to iset.mm

* copy ringsrg from set.mm to iset.mm

* copy ring1eq0 from set.mm to iset.mm

* add ring1ne0 to mmil.html

* copy ringinvnz1ne0 from set.mm to iset.mm

* copy ringinvnzdiv from set.mm to iset.mm

* Add ringnegl and rngnegr to iset.mm

Copied from set.mm with the only change being to the comments, to avoid
references to theorems not in iset.mm.

* copy ringmneg1 from set.mm to iset.mm

* copy ringmneg2 from set.mm to iset.mm

* copy ringm2neg from set.mm to iset.mm

* copy ringsubdi from set.mm to iset.mm

* copy rngsubdir from set.mm to iset.mm

* copy mulgass2 from set.mm to iset.mm

* Add grppropstrg to iset.mm

This is grppropstr from set.mm with an additional set existence
condition.  The proof is based on the set.mm proof.

* Add ring1 to iset.mm

Stated as in set.mm.  The proof needs a decent amount of intuitionizing
but is basically the set.mm proof.

* copy ringn0 from set.mm to iset.mm

The only change is to the comment, to reflect not empty versus
inhabited.

* add ringlghm , ringrghm to mmil.html

* add finSupp and gsum theorems to mmil.html

This is gsummulc1 , gsummulc2 , gsummgp0 , and gsumdixp

* Add structure product theorems to mmil.html

This is prdsmgp , prdsmulrcl , prdsringd , prdscrngd , and prds1

* Add structure power theorems to mmil.html

This is pwsring , pws1 , pwscrng , and pwsmgp

* add imasring to mmil.html

* add qusring2 to mmil.html

* add crngbinom to mmil.html

iset.mm

@@ -145375,6 +145375,23 @@ an algebraic structure formed from a base set of elements (notated
       UEUCHSSUFUGUDUEDTOUAUB $.
   $}
 
+  ${
+    $d B x y $.  $d K x y $.  $d L x y $.  $d V x y $.
+    grppropstr.b $e |- ( Base ` K ) = B $.
+    grppropstr.p $e |- ( +g ` K ) = .+ $.
+    grppropstr.l $e |- L
+          = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } $.
+    $( Generalize a specific 2-element group ` L ` to show that any set ` K `
+       with the same (relevant) properties is also a group.  (Contributed by
+       NM, 28-Oct-2012.)  (Revised by Mario Carneiro, 6-Jan-2015.) $)
+    grppropstrg $p |- ( K e. V -> ( K e. Grp <-> L e. Grp ) ) $=
+      ( vx vy wcel cbs cfv cvv wceq eqeltrrid cplusg syl2anc eqtrid cv wfn elex
+      basfn funfvex funfni plusgslid slotex grpbaseg eqtr4d wa grpplusgg oveqdr
+      sylancr grppropd ) CEKZIJACDUOADLMZCLMZUOANKZBNKZAUPOUOAUQNFUOLNUACNKUQNK
+      ZUCCEUBUTNCLCLUDUEUMPZUOBCQMZNGCQEUFUGPZABDNNHUHRZUOUQAUPFVDSUIVDUOITAKJT
+      AKUJIJVBDQMZUOVBBVEGUOURUSBVEOVAVCABDNNHUKRSULUN $.
+  $}
+
   ${
     $d x y .+ $.  $d y .0. $.  $d x y B $.  $d x y G $.  $d x y ph $.
     $d y N $.
@@ -149042,6 +149059,290 @@ the additive structure must be abelian (see ~ ringcom ), care must be
       RUAUSGVCVGUTVA $.
   $}
 
+  ${
+    rngz.b $e |- B = ( Base ` R ) $.
+    rngz.t $e |- .x. = ( .r ` R ) $.
+    rngz.z $e |- .0. = ( 0g ` R ) $.
+    $( The zero of a unital ring is a left-absorbing element.  (Contributed by
+       FL, 31-Aug-2009.) $)
+    ringlz $p |- ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .0. ) $=
+      ( crg wcel wa co cplusg cfv wceq cgrp ringgrp grpidcl eqid adantr w3a syl
+      grplid syl2anc2 oveq1d simpr ringdir syldan ringcl syl3anc grprid syl2anc
+      3jca simpl eqcomd 3eqtr3d wb grplcan syl13anc mpbid ) BIJZDAJZKZEDCLZVDBM
+      NZLZVDEVELZOZVDEOZVCEEVELZDCLZVDVFVGVCVJEDCVAVJEOZVBVABPJZEAJZVLBQZABEFHR
+      ZAVEBEEFVESZHUCUDTUEVAVBVNVNVBUAVKVFOVCVNVNVBVAVNVBVAVMVNVOVPUBTZVRVAVBUF
+      ZUMAVEBCEEDFVQGUGUHVCVMVDAJZVDVGOVAVMVBVOTZVCVAVNVBVTVAVBUNVRVSABCEDFGUIU
+      JZVMVTKVGVDAVEBVDEFVQHUKUOULUPVCVMVTVNVTVHVIUQWAWBVRWBAVEBVDEVDFVQURUSUT
+      $.
+
+    $( The zero of a unital ring is a right-absorbing element.  (Contributed by
+       FL, 31-Aug-2009.) $)
+    ringrz $p |- ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. ) $=
+      ( crg wcel wa co cplusg cfv wceq cgrp ringgrp grpidcl grplid adantr simpr
+      eqid syl2anc2 oveq2d w3a 3jca ringdi syldan ringcl mpd3an3 eqcomd syl2anc
+      syl 3eqtr3d wb grprcan syl13anc mpbid ) BIJZDAJZKZDECLZVBBMNZLZEVBVCLZOZV
+      BEOZVADEEVCLZCLZVBVDVEVAVHEDCUSVHEOZUTUSBPJZEAJZVJBQZABEFHRZAVCBEEFVCUBZH
+      SUCTUDUSUTUTVLVLUEVIVDOVAUTVLVLUSUTUAUSVLUTUSVKVLVMVNUMTZVPUFAVCBCDEEFVOG
+      UGUHVAVKVBAJZVBVEOUSVKUTVMTZUSUTVLVQVPABCDEFGUIUJZVKVQKVEVBAVCBVBEFVOHSUK
+      ULUNVAVKVQVLVQVFVGUOVRVSVPVSAVCBVBEVBFVOUPUQUR $.
+  $}
+
+  ${
+    $d x y z R $.
+    $( Any ring is also a semiring.  (Contributed by Thierry Arnoux,
+       1-Apr-2018.) $)
+    ringsrg $p |- ( R e. Ring -> R e. SRing ) $=
+      ( vx vy vz crg wcel ccmn cmgp cfv cmnd cv cplusg co cmulr wceq wa cbs c0g
+      wral eqid csrg ringcmn ringmgp isring simp3bi ringlz ringrz jca ralrimiva
+      cgrp r19.26 sylanbrc issrg syl3anbrc ) AEFZAGFAHIZJFZBKZCKZDKZALIZMANIZMU
+      RUSVBMURUTVBMZVAMOURUSVAMUTVBMVCUSUTVBMVAMOPDAQIZSCVDSZARIZURVBMVFOZURVFV
+      BMVFOZPZPBVDSZAUAFAUBAUPUPTZUCUOVEBVDSZVIBVDSVJUOAUJFUQVLBCDVDVAAVBUPVDTZ
+      VKVATZVBTZUDUEUOVIBVDUOURVDFPVGVHVDAVBURVFVMVOVFTZUFVDAVBURVFVMVOVPUGUHUI
+      VEVIBVDUKULBCDVDVAAVBUPVFVMVKVNVOVPUMUN $.
+  $}
+
+  ${
+    ring1eq0.b $e |- B = ( Base ` R ) $.
+    ring1eq0.u $e |- .1. = ( 1r ` R ) $.
+    ring1eq0.z $e |- .0. = ( 0g ` R ) $.
+    $( If one and zero are equal, then any two elements of a ring are equal.
+       Alternately, every ring has one distinct from zero except the zero ring
+       containing the single element ` { 0 } ` .  (Contributed by Mario
+       Carneiro, 10-Sep-2014.) $)
+    ring1eq0 $p |- ( ( R e. Ring /\ X e. B /\ Y e. B ) ->
+      ( .1. = .0. -> X = Y ) ) $=
+      ( crg wcel w3a wceq wa co oveq1d ringlz syl2anc eqtr4d ringlidm cmulr cfv
+      simpr simpl1 simpl2 eqid simpl3 3eqtr3d ex ) BJKZDAKZEAKZLZCFMZDEMUMUNNZC
+      DBUAUBZOZCEUPOZDEUOUQFDUPOZURUOCFDUPUMUNUCZPUOURFEUPOZUSUOCFEUPUTPUOUSFVA
+      UOUJUKUSFMUJUKULUNUDZUJUKULUNUEZABUPDFGUPUFZIQRUOUJULVAFMVBUJUKULUNUGZABU
+      PEFGVDIQRSSSUOUJUKUQDMVBVCABUPCDGVDHTRUOUJULUREMVBVEABUPCEGVDHTRUHUI $.
+  $}
+
+  ${
+    $d X a $.  $d .0. a $.  $d .1. a $.  $d .x. a $.  $d ph a $.
+    ringinvnzdiv.b $e |- B = ( Base ` R ) $.
+    ringinvnzdiv.t $e |- .x. = ( .r ` R ) $.
+    ringinvnzdiv.u $e |- .1. = ( 1r ` R ) $.
+    ringinvnzdiv.z $e |- .0. = ( 0g ` R ) $.
+    ringinvnzdiv.r $e |- ( ph -> R e. Ring ) $.
+    ringinvnzdiv.x $e |- ( ph -> X e. B ) $.
+    ringinvnzdiv.a $e |- ( ph -> E. a e. B ( a .x. X ) = .1. ) $.
+    $( In a unitary ring, a left invertible element is different from zero iff
+       ` .1. =/= .0. ` .  (Contributed by FL, 18-Apr-2010.)  (Revised by AV,
+       24-Aug-2021.) $)
+    ringinvnz1ne0 $p |- ( ph -> ( X =/= .0. <-> .1. =/= .0. ) ) $=
+      ( co wceq wcel wa oveq2 cv wb wi ringrz sylan eqeq12 biimpd ex mpan9 syl5
+      crg ringridm eqeq12d syl2anc ad2antrr impbid r19.29a necon3bid ) AFGEGAHU
+      AZFDPZEQZFGQZEGQZUBHBAUSBRZSZVASZVBVCVBUTUSGDPZQZVFVCFGUSDTVEVGGQZVAVHVCU
+      CZACUKRZVDVIMBCDUSGIJLUDUEVAVIVJVAVISVHVCUTEVGGUFUGUHUIUJVCFEDPZFGDPZQZVF
+      VBEGFDTAVNVBUCZVDVAAVKFBRZVOMNVKVPSZVNVBVQVLFVMGBCDEFIJKULBCDFGIJLUDUMUGU
+      NUOUJUPOUQUR $.
+
+    $d Y a $.
+    ringinvnzdiv.y $e |- ( ph -> Y e. B ) $.
+    $( In a unitary ring, a left invertible element is not a zero divisor.
+       (Contributed by FL, 18-Apr-2010.)  (Revised by Jeff Madsen,
+       18-Apr-2010.)  (Revised by AV, 24-Aug-2021.) $)
+    ringinvnzdiv $p |- ( ph -> ( ( X .x. Y ) = .0. <-> Y = .0. ) ) $=
+      ( co wceq adantr cv wrex wi wcel wa crg ringlidm syl2anc eqcomd ad3antrrr
+      oveq1 eqcoms adantl w3a simpr 3jca jca ringass syl eqtrd ringrz sylan9eqr
+      oveq2 sylan 3eqtrd exp31 rexlimdva mpd ex impbid ) AFGDRZHSZGHSZAIUAZFDRZ
+      ESZIBUBVLVMUCZPAVPVQIBAVNBUDZUEZVPVLVMVSVPUEZVLUEGEGDRZVNVKDRZHAGWASVRVPV
+      LAWAGACUFUDZGBUDZWAGSNQBCDEGJKLUGUHUIUJVTWAWBSVLVTWAVOGDRZWBVPWAWESZVSWFE
+      VOEVOGDUKULUMVTWCVRFBUDZWDUNZUEZWEWBSVSWIVPVSWCWHAWCVRNTVSVRWGWDAVRUOAWGV
+      ROTAWDVRQTUPUQTBCDVNFGJKURUSUTTVLVTWBVNHDRZHVKHVNDVCVSWJHSZVPAWCVRWKNBCDV
+      NHJKMVAVDTVBVEVFVGVHAVMVLVMAVKFHDRZHGHFDVCAWCWGWLHSNOBCDFHJKMVAUHVBVIVJ
+      $.
+  $}
+
+  ${
+    ringnegl.b $e |- B = ( Base ` R ) $.
+    ringnegl.t $e |- .x. = ( .r ` R ) $.
+    ringnegl.u $e |- .1. = ( 1r ` R ) $.
+    ringnegl.n $e |- N = ( invg ` R ) $.
+    ringnegl.r $e |- ( ph -> R e. Ring ) $.
+    ringnegl.x $e |- ( ph -> X e. B ) $.
+    $( Negation in a ring is the same as left multiplication by -1.
+       (Contributed by Jeff Madsen, 19-Jun-2010.)  (Revised by Mario Carneiro,
+       2-Jul-2014.) $)
+    ringnegl $p |- ( ph -> ( ( N ` .1. ) .x. X ) = ( N ` X ) ) $=
+      ( cfv co wceq wcel syl syl2anc eqid cplusg c0g crg ringidcl cgrp grpinvcl
+      ringgrp ringdir syl13anc grprinv oveq1d ringlz eqtrd ringlidm 3eqtr3rd wb
+      ringcl syl3anc grpinvid1 mpbird eqcomd ) AGFNZEFNZGDOZAVBVDPZGVDCUANZOZCU
+      BNZPZAEVCVFOZGDOZEGDOZVDVFOZVHVGACUCQZEBQZVCBQZGBQZVKVMPLAVNVOLBCEHJUDRZA
+      CUEQZVOVPAVNVSLCUGRZVRBCFEHKUFSZMBVFCDEVCGHVFTZIUHUIAVKVHGDOZVHAVJVHGDAVS
+      VOVJVHPVTVRBVFCFEVHHWBVHTZKUJSUKAVNVQWCVHPLMBCDGVHHIWDULSUMAVLGVDVFAVNVQV
+      LGPLMBCDEGHIJUNSUKUOAVSVQVDBQZVEVIUPVTMAVNVPVQWELWAMBCDVCGHIUQURBVFCFGVDV
+      HHWBWDKUSURUTVA $.
+
+    $( Negation in a ring is the same as right multiplication by -1.
+       (Contributed by Jeff Madsen, 19-Jun-2010.)  (Revised by Mario Carneiro,
+       2-Jul-2014.) $)
+    rngnegr $p |- ( ph -> ( X .x. ( N ` .1. ) ) = ( N ` X ) ) $=
+      ( cfv co wceq wcel syl syl2anc eqid cplusg c0g crg cgrp ringidcl grpinvcl
+      ringgrp ringdi syl13anc grplinv oveq2d ringrz ringridm 3eqtr3rd wb ringcl
+      eqtrd syl3anc grpinvid2 mpbird eqcomd ) AGFNZGEFNZDOZAVBVDPZVDGCUANZOZCUB
+      NZPZAGVCEVFOZDOZVDGEDOZVFOZVHVGACUCQZGBQZVCBQZEBQZVKVMPLMACUDQZVQVPAVNVRL
+      CUGRZAVNVQLBCEHJUERZBCFEHKUFSZVTBVFCDGVCEHVFTZIUHUIAVKGVHDOZVHAVJVHGDAVRV
+      QVJVHPVSVTBVFCFEVHHWBVHTZKUJSUKAVNVOWCVHPLMBCDGVHHIWDULSUQAVLGVDVFAVNVOVL
+      GPLMBCDEGHIJUMSUKUNAVRVOVDBQZVEVIUOVSMAVNVOVPWELMWABCDGVCHIUPURBVFCFGVDVH
+      HWBWDKUSURUTVA $.
+  $}
+
+  ${
+    ringneglmul.b $e |- B = ( Base ` R ) $.
+    ringneglmul.t $e |- .x. = ( .r ` R ) $.
+    ringneglmul.n $e |- N = ( invg ` R ) $.
+    ringneglmul.r $e |- ( ph -> R e. Ring ) $.
+    ringneglmul.x $e |- ( ph -> X e. B ) $.
+    ringneglmul.y $e |- ( ph -> Y e. B ) $.
+    $( Negation of a product in a ring.  ( ~ mulneg1 analog.)  (Contributed by
+       Jeff Madsen, 19-Jun-2010.)  (Revised by Mario Carneiro, 2-Jul-2014.) $)
+    ringmneg1 $p |- ( ph -> ( ( N ` X ) .x. Y ) = ( N ` ( X .x. Y ) ) ) $=
+      ( cur cfv co crg wcel syl ringnegl wceq ringgrp ringidcl grpinvcl syl2anc
+      cgrp eqid ringass syl13anc oveq1d ringcl syl3anc 3eqtr3d ) ACNOZEOZFDPZGD
+      PZUOFGDPZDPZFEOZGDPUREOACQRZUOBRZFBRZGBRZUQUSUAKACUFRZUNBRZVBAVAVEKCUBSAV
+      AVFKBCUNHUNUGZUCSBCEUNHJUDUELMBCDUOFGHIUHUIAUPUTGDABCDUNEFHIVGJKLTUJABCDU
+      NEURHIVGJKAVAVCVDURBRKLMBCDFGHIUKULTUM $.
+
+    $( Negation of a product in a ring.  ( ~ mulneg2 analog.)  (Contributed by
+       Jeff Madsen, 19-Jun-2010.)  (Revised by Mario Carneiro, 2-Jul-2014.) $)
+    ringmneg2 $p |- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) ) $=
+      ( co cur cfv crg wcel syl rngnegr wceq cgrp ringgrp eqid ringidcl syl2anc
+      grpinvcl ringass syl13anc ringcl syl3anc oveq2d 3eqtr3rd ) AFGDNZCOPZEPZD
+      NZFGUPDNZDNZUNEPFGEPZDNACQRZFBRZGBRZUPBRZUQUSUAKLMACUBRZUOBRZVDAVAVEKCUCS
+      AVAVFKBCUOHUOUDZUESBCEUOHJUGUFBCDFGUPHIUHUIABCDUOEUNHIVGJKAVAVBVCUNBRKLMB
+      CDFGHIUJUKTAURUTFDABCDUOEGHIVGJKMTULUM $.
+
+    $( Double negation of a product in a ring.  ( ~ mul2neg analog.)
+       (Contributed by Mario Carneiro, 4-Dec-2014.) $)
+    ringm2neg $p |- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) ) $=
+      ( cfv co cgrp wcel crg ringgrp syl2anc syl grpinvcl ringmneg1 fveq2d wceq
+      ringmneg2 ringcl syl3anc grpinvinv 3eqtrd ) AFENGENZDOFUKDOZENFGDOZENZENZ
+      UMABCDEFUKHIJKLACPQZGBQZUKBQACRQZUPKCSUAZMBCEGHJUBTUCAULUNEABCDEFGHIJKLMU
+      FUDAUPUMBQZUOUMUEUSAURFBQUQUTKLMBCDFGHIUGUHBCEUMHJUITUJ $.
+  $}
+
+  ${
+    ringsubdi.b $e |- B = ( Base ` R ) $.
+    ringsubdi.t $e |- .x. = ( .r ` R ) $.
+    ringsubdi.m $e |- .- = ( -g ` R ) $.
+    ringsubdi.r $e |- ( ph -> R e. Ring ) $.
+    ringsubdi.x $e |- ( ph -> X e. B ) $.
+    ringsubdi.y $e |- ( ph -> Y e. B ) $.
+    ringsubdi.z $e |- ( ph -> Z e. B ) $.
+    $( Ring multiplication distributes over subtraction.  ( ~ subdi analog.)
+       (Contributed by Jeff Madsen, 19-Jun-2010.)  (Revised by Mario Carneiro,
+       2-Jul-2014.) $)
+    ringsubdi $p |- ( ph ->
+      ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) ) $=
+      ( cfv co wcel wceq syl2anc cminusg cplusg crg ringgrp syl grpinvcl ringdi
+      cgrp syl13anc ringmneg2 oveq2d eqtrd grpsubval ringcl syl3anc 3eqtr4d
+      eqid ) AFGHCUAPZPZCUBPZQZDQZFGDQZFHDQZURPZUTQZFGHEQZDQVCVDEQZAVBVCFUSDQZU
+      TQZVFACUCRZFBRZGBRZUSBRZVBVJSLMNACUHRZHBRZVNAVKVOLCUDUEOBCURHIURUQZUFTBUT
+      CDFGUSIUTUQZJUGUIAVIVEVCUTABCDURFHIJVQLMOUJUKULAVGVAFDAVMVPVGVASNOBUTCURE
+      GHIVRVQKUMTUKAVCBRZVDBRZVHVFSAVKVLVMVSLMNBCDFGIJUNUOAVKVLVPVTLMOBCDFHIJUN
+      UOBUTCUREVCVDIVRVQKUMTUP $.
+
+    $( Ring multiplication distributes over subtraction.  ( ~ subdir analog.)
+       (Contributed by Jeff Madsen, 19-Jun-2010.)  (Revised by Mario Carneiro,
+       2-Jul-2014.) $)
+    rngsubdir $p |- ( ph ->
+      ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) ) $=
+      ( cfv co wcel wceq syl2anc cminusg crg cgrp ringgrp eqid grpinvcl ringdir
+      cplusg syl ringmneg1 oveq2d eqtrd grpsubval oveq1d ringcl syl3anc 3eqtr4d
+      syl13anc ) AFGCUAPZPZCUHPZQZHDQZFHDQZGHDQZUSPZVAQZFGEQZHDQVDVEEQZAVCVDUTH
+      DQZVAQZVGACUBRZFBRZUTBRZHBRZVCVKSLMACUCRZGBRZVNAVLVPLCUDUINBCUSGIUSUEZUFT
+      OBVACDFUTHIVAUEZJUGURAVJVFVDVAABCDUSGHIJVRLNOUJUKULAVHVBHDAVMVQVHVBSMNBVA
+      CUSEFGIVSVRKUMTUNAVDBRZVEBRZVIVGSAVLVMVOVTLMOBCDFHIJUOUPAVLVQVOWALNOBCDGH
+      IJUOUPBVACUSEVDVEIVSVRKUMTUQ $.
+  $}
+
+  ${
+    $d x y B $.  $d x y R $.  $d x y .x. $.  $d x y .X. $.  $d x y X $.
+    $d x N $.  $d x y Y $.
+    mulgass2.b $e |- B = ( Base ` R ) $.
+    mulgass2.m $e |- .x. = ( .g ` R ) $.
+    mulgass2.t $e |- .X. = ( .r ` R ) $.
+    $( An associative property between group multiple and ring multiplication.
+       (Contributed by Mario Carneiro, 14-Jun-2015.) $)
+    mulgass2 $p |- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) ->
+      ( ( N .x. X ) .X. Y ) = ( N .x. ( X .X. Y ) ) ) $=
+      ( wcel co wceq cc0 oveq1 oveq1d eqeq12d cfv adantr syl3anc vx vy cz wi cv
+      crg cneg caddc w3a c0g eqid ringlz 3adant3 simp3 mulg0 syl ringcl 3eqtr4d
+      c1 3com23 cn0 wa cplusg cgrp simpl1 ringgrp adantl mulgp1 3ad2ant1 mulgcl
+      nn0z simpl2 ringdir syl13anc eqtrd syl5ibr ex cminusg fveq2 nnz ringmneg1
+      cn mulgneg zindd 3exp com24 3imp2 ) BUFKZEUCKZFAKZGAKZEFCLZGDLZEFGDLZCLZM
+      ZWHWKWJWIWPWHWKWJWIWPUDUAUEZFCLZGDLZWQWNCLZMNFCLZGDLZNWNCLZMUBUEZFCLZGDLZ
+      XDWNCLZMZXDUGZFCLZGDLZXIWNCLZMZXDUSUHLZFCLZGDLZXNWNCLZMZWPWHWKWJUIZUAUBEW
+      QNMZWSXBWTXCXTWRXAGDWQNFCOPWQNWNCOQWQXDMZWSXFWTXGYAWRXEGDWQXDFCOPWQXDWNCO
+      QWQXNMZWSXPWTXQYBWRXOGDWQXNFCOPWQXNWNCOQWQXIMZWSXKWTXLYCWRXJGDWQXIFCOPWQX
+      IWNCOQWQEMZWSWMWTWOYDWRWLGDWQEFCOPWQEWNCOQXSBUJRZGDLZYEXBXCWHWKYFYEMWJABD
+      GYEHJYEUKZULUMXSXAYEGDXSWJXAYEMWHWKWJUNZACBFYEHYGIUOUPPXSWNAKZXCYEMWHWJWK
+      YIABDFGHJUQUTZACBWNYEHYGIUOUPURXSXDVAKZXHXRUDXHXRXSYKVBZXFWNBVCRZLZXGWNYM
+      LZMXFXGWNYMOYLXPYNXQYOYLXPXEFYMLZGDLZYNYLXOYPGDYLBVDKZXDUCKZWJXOYPMYLWHYR
+      WHWKWJYKVEZBVFZUPZYKYSXSXDVKVGZXSWJYKYHSZAYMCBXDFHIYMUKZVHTPYLWHXEAKZWJWK
+      YQYNMYTYLYRYSWJUUFXSYRYKWHWKYRWJUUAVIZSUUCUUDACBXDFHIVJZTUUDWHWKWJYKVLAYM
+      BDXEFGHUUEJVMVNVOYLYRYSYIXQYOMUUBUUCXSYIYKYJSAYMCBXDWNHIUUEVHTQVPVQXSXDWB
+      KZXHXMUDXHXMXSUUIVBZXFBVRRZRZXGUUKRZMXFXGUUKVSUUJXKUULXLUUMUUJXKXEUUKRZGD
+      LUULUUJXJUUNGDUUJYRYSWJXJUUNMXSYRUUIUUGSZUUIYSXSXDVTVGZXSWJUUIYHSZACBUUKX
+      DFHIUUKUKZWCTPUUJABDUUKXEGHJUURWHWKWJUUIVEUUJYRYSWJUUFUUOUUPUUQUUHTWHWKWJ
+      UUIVLWAVOUUJYRYSYIXLUUMMUUOUUPXSYIUUIYJSACBUUKXDWNHIUURWCTQVPVQWDWEWFWG
+      $.
+  $}
+
+  ${
+    $d Z a b c x y $.  $d M a b c x y $.  $d V a b c x y $.
+    ring1.m $e |- M = { <. ( Base ` ndx ) , { Z } >. ,
+                       <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. ,
+                       <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. } $.
+    $( The (smallest) structure representing a _zero ring_.  (Contributed by
+       AV, 28-Apr-2019.) $)
+    ring1 $p |- ( Z e. V -> M e. Ring ) $=
+      ( va vb vc wcel cfv cv cop co wceq wa wral cplusg cvv eqid cn eqeq12d csn
+      vx cgrp cmgp cmnd w3a crg cnx cbs cpr snexg opexg anidms mpancom rngbaseg
+      vy syl syl3anc opeq2d rngplusgg preq12d grp1 eqeltrrd cmulr ctp basendxnn
+      sylancr cslot plusgslid simpri mulrslid tpexg eqeltrid grppropstrg mpbird
+      mnd1 eqidd grpbaseg syl2anc mgpbasg 3eqtr3rd rngmulrg grpplusgg mgpplusgg
+      wb oveqdr mndpropd df-ov fvsng eqtrid oveq2d oveq12d eqtr4d oveq1 anbi12d
+      oveq1d 2ralbidv ralsng oveq2 ralbidv 3bitrd mpbir2and 3jca oveqd oveq123d
+      raleqbidv 3anbi3d isring bitr4di mpbid ) CBHZAUCHZAUDIZUEHZEJZFJZGJZCCKZC
+      KZUAZLZXTLZXOXPXTLZXOXQXTLZXTLZMZYCXQXTLZYDYAXTLZMZNZGCUAZOZFYKOZEYKOZUFZ
+      AUGHZXKXLXNYNXKXLUHUIIZAUIIZKZUHPIZAPIZKZUJZUCHZXKYQYKKZYTXTKZUJZUUCUCXKU
+      UEYSUUFUUBXKYKYRYQXKYKQHZXTQHZUUIYKYRMCBUKZXKXSQHZUUIXRQHZXKUUKXKUULCCBBU
+      LUMZXRCQBULUNXSQUKUQZUUNYKXTAXTQQQDUOURZUSXKXTUUAYTXKUUHUUIUUIXTUUAMUUJUU
+      NUUNYKXTAXTQQQDUTURZUSVACUUGBUUGRZVBVCXKAQHZXLUUDWEXKAUUEUUFUHVDIZXTKZVEZ
+      QDXKUUEQHZUUFQHZUUTQHZUVAQHXKYQSHUUHUVBVFUUJYQYKSQULVGXKYTSHZUUIUVCPYTVHM
+      UVEVIVJUUNYTXTSQULVGXKUUSSHZUUIUVDVDUUSVHMUVFVKVJUUNUUSXTSQULVGUUEUUFUUTQ
+      QQVLURVMZYRUUAAUUCQYRRZUUARZUUCRVNUQVOXKXNUUGUEHCUUGBUUQVPXKUBUPXMUIIZXMU
+      UGXKUVJVQXKYKYRUUGUIIZUVJUUOXKUUHUUIYKUVKMUUJUUNYKXTUUGQQUUQVRVSXKUURYRUV
+      JMUVGYRAXMQXMRZUVHVTUQWAXKUBJUVJHUPJUVJHNUBUPXMPIZUUGPIZXKXTAVDIZUVNUVMXK
+      UUHUUIUUIXTUVOMUUJUUNUUNYKXTAXTQQQDWBURZXKUUHUUIXTUVNMUUJUUNYKXTUUGQQUUQW
+      CVSXKUURUVOUVMMUVGAUVOXMQUVLUVORZWDUQWAWFWGVOXKYNCCCXTLZXTLZUVRUVRXTLZMZU
+      VRCXTLZUVTMZXKUVSUVRUVTXKUVRCCXTXKUVRXRXTIZCCCXTWHUULXKUWDCMUUMXRCQBWIUNW
+      JZWKXKUVRCUVRCXTUWEUWEWLZWMXKUWBUVRUVTXKUVRCCXTUWEWPUWFWMXKYNCYAXTLZCXPXT
+      LZCXQXTLZXTLZMZUWHXQXTLZUWIYAXTLZMZNZGYKOZFYKOZCUWIXTLZUVRUWIXTLZMZUVRXQX
+      TLZUWIUWIXTLZMZNZGYKOZUWAUWCNZYMUWQECBXOCMZYJUWOFGYKYKUXGYFUWKYIUWNUXGYBU
+      WGYEUWJXOCYAXTWNUXGYCUWHYDUWIXTXOCXPXTWNZXOCXQXTWNZWLTUXGYGUWLYHUWMUXGYCU
+      WHXQXTUXHWPUXGYDUWIYAXTUXIWPTWOWQWRUWPUXEFCBXPCMZUWOUXDGYKUXJUWKUWTUWNUXC
+      UXJUWGUWRUWJUWSUXJYAUWICXTXPCXQXTWNZWKUXJUWHUVRUWIXTXPCCXTWSZWPTUXJUWLUXA
+      UWMUXBUXJUWHUVRXQXTUXLWPUXJYAUWIUWIXTUXKWKTWOWTWRUXDUXFGCBXQCMZUWTUWAUXCU
+      WCUXMUWRUVSUWSUVTUXMUWIUVRCXTXQCCXTWSZWKUXMUWIUVRUVRXTUXNWKTUXMUXAUWBUXBU
+      VTXQCUVRXTWSUXMUWIUVRUWIUVRXTUXNUXNWLTWOWRXAXBXCXKYOXLXNXOXPXQUUALZUVOLZX
+      OXPUVOLZXOXQUVOLZUUALZMZXOXPUUALZXQUVOLZUXRXPXQUVOLZUUALZMZNZGYROZFYROZEY
+      ROZUFYPXKYNUYIXLXNXKYMUYHEYKYRUUOXKYLUYGFYKYRUUOXKYJUYFGYKYRUUOXKYFUXTYIU
+      YEXKYBUXPYEUXSXKXOXOYAUXOXTUVOUVPXKXOVQXKXTUUAXPXQUUPXDXEXKYCUXQYDUXRXTUU
+      AUUPXKXTUVOXOXPUVPXDXKXTUVOXOXQUVPXDZXETXKYGUYBYHUYDXKYCUYAXQXQXTUVOUVPXK
+      XTUUAXOXPUUPXDXKXQVQXEXKYDUXRYAUYCXTUUAUUPUYJXKXTUVOXPXQUVPXDXETWOXFXFXFX
+      GEFGYRUUAAUVOXMUVHUVLUVIUVQXHXIXJ $.
+  $}
+
+  $( The class of rings is not empty (it is also inhabited, as shown at
+     ~ ring1 ).  (Contributed by AV, 29-Apr-2019.) $)
+  ringn0 $p |- Ring =/= (/) $=
+    ( vz cv cvv wcel cnx cbs cfv csn cop cplusg cmulr ctp crg c0 wne eqid ring1
+    vex ne0i mp2b ) ABZCDEFGUAHIEJGUAUAIUAIHZIEKGUBILZMDMNOARUCCUAUCPQMUCST $.
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#

mmil.raw.html

@@ -10533,9 +10533,7 @@
 
 <tr>
   <td>grppropstr</td>
-  <td><i>none</i></td>
-  <td>The forward direction seems provable; the reverse
-  direction might need a ` K e. _V ` condition.</td>
+  <td>~ grppropstrg</td>
 </tr>
 
 <tr>
@@ -10764,6 +10762,66 @@
   <td>the set.mm proof uses ressbas2 and ressplusg</td>
 </tr>
 
+<tr>
+  <td>ring1ne0</td>
+  <td><i>none</i></td>
+  <td>probably provable but the set.mm proof uses hashgt12el</td>
+</tr>
+
+<tr>
+  <td>ringlghm , ringrghm</td>
+  <td><i>none</i></td>
+  <td>depend on GrpHom ( df-ghm )</td>
+</tr>
+
+<tr>
+  <td>gsummulc1 , gsummulc2</td>
+  <td><i>none</i></td>
+  <td>depend on finSupp and gsum theorems we do not have</td>
+</tr>
+
+<tr>
+  <td>gsummgp0</td>
+  <td><i>none</i></td>
+  <td>depends on gsum theorems we do not have</td>
+</tr>
+
+<tr>
+  <td>gsumdixp</td>
+  <td><i>none</i></td>
+  <td>depends on finSupp and gsum theorems we do not have</td>
+</tr>
+
+<tr>
+  <td>prdsmgp , prdsmulrcl , prdsringd , prdscrngd , prds1</td>
+  <td><i>none</i></td>
+  <td>depend on various structure product theorems</td>
+</tr>
+
+<tr>
+  <td>pwsring , pws1 , pwscrng , pwsmgp</td>
+  <td><i>none</i></td>
+  <td>depend on various structure power theorems</td>
+</tr>
+
+<tr>
+  <td>imasring</td>
+  <td><i>none</i></td>
+  <td>depends on various image structure theorems</td>
+</tr>
+
+<tr>
+  <td>qusring2</td>
+  <td><i>none</i></td>
+  <td>depends on various quotient structure theorems</td>
+</tr>
+
+<tr>
+  <td>crngbinom</td>
+  <td><i>none</i></td>
+  <td>depends on various ` gsum ` theorems</td>
+</tr>
+
 <tr>
   <td>df-drng</td>
   <td><i>none</i></td>