Theorem crngring 18558

Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
crngring	|- ( R e. CRing -> R e. Ring )

Proof of Theorem crngring

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- (mulGrp ` R ) = (mulGrp ` R )
2	1	iscrng 18554	. 2 |- ( R e. CRing <-> ( R e. Ring /\ (mulGrp ` R ) e. CMnd ) )
3	2	simplbi 476	1 |- ( R e. CRing -> R e. Ring )

Syntax hints:   -> wi 4   e. wcel 1990   ` cfv 5888  CMndccmn 18193  mulGrpcmgp 18489   Ringcrg 18547   CRingccrg 18548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-cring 18550

This theorem is referenced by:  gsummgp0  18608  prdscrngd  18613  crngbinom  18621  dvdsunit  18663  unitmulclb  18665  unitabl  18668  idsrngd  18862  rmodislmod  18931  quscrng  19240  assa2ass  19322  sraassa  19325  rlmassa  19326  asclrhm  19342  assamulgscmlem2  19349  psrcrng  19413  psrassa  19414  mplcrng  19453  mplassa  19454  mplcoe2  19469  mplbas2  19470  mplmon2mul  19501  mplind  19502  evlslem2  19512  evlslem6  19513  evlslem3  19514  evlslem1  19515  evlseu  19516  evlsval2  19520  evlrhm  19525  evlsscasrng  19526  evlsca  19527  evlsvarsrng  19528  evlvar  19529  mpfind  19536  ply1crng  19568  ply1assa  19569  lply1binom  19676  lply1binomsc  19677  evls1rhmlem  19686  evls1gsumadd  19689  evls1gsummul  19690  evl1val  19693  evl1sca  19698  evl1scad  19699  evl1var  19700  evl1vard  19701  evls1var  19702  evls1scasrng  19703  evls1varsrng  19704  evl1subd  19706  evl1expd  19709  pf1const  19710  pf1id  19711  pf1ind  19719  evl1gsumdlem  19720  evl1gsumd  19721  evl1gsumadd  19722  evl1gsummul  19724  evl1varpw  19725  evl1scvarpw  19727  evl1scvarpwval  19728  evl1gsummon  19729  cnring  19768  zringring  19821  zring0  19828  znzrh2  19894  zncyg  19897  zndvds0  19899  znf1o  19900  zzngim  19901  znfld  19909  znchr  19911  znunit  19912  znrrg  19914  cygznlem3  19918  re0g  19958  mamuvs2  20212  matassa  20250  madetsumid  20267  madetsmelbas  20270  madetsmelbas2  20271  mat1dimcrng  20283  dmatcrng  20308  scmatcrng  20327  mdetleib2  20394  mdetf  20401  m1detdiag  20403  mdetdiaglem  20404  mdetdiag  20405  mdet1  20407  mdetrlin  20408  mdetrsca  20409  mdetrsca2  20410  mdetr0  20411  mdet0  20412  mdetrlin2  20413  mdetralt  20414  mdetero  20416  mdetmul  20429  maducoeval2  20446  maduf  20447  madutpos  20448  madugsum  20449  madurid  20450  madulid  20451  marep01ma  20466  smadiadetlem0  20467  smadiadetlem1a  20469  smadiadetlem3lem2  20473  smadiadetlem3  20474  smadiadetlem4  20475  smadiadet  20476  smadiadetglem1  20477  smadiadetglem2  20478  smadiadetg  20479  matinv  20483  matunit  20484  slesolinv  20486  slesolinvbi  20487  slesolex  20488  cramerimplem1  20489  cramerimplem2  20490  cramerimplem3  20491  cramerimp  20492  cramer  20497  mat2pmatmul  20536  mat2pmatmhm  20538  mat2pmatrhm  20539  mat2pmatlin  20540  m2cpmmhm  20550  m2cpmrhm  20551  m2pmfzgsumcl  20553  m2cpmrngiso  20563  monmatcollpw  20584  pmatcollpwlem  20585  pmatcollpw  20586  pmatcollpwfi  20587  pmatcollpw3fi1lem2  20592  pmatcollpwscmat  20596  monmat2matmon  20629  pm2mp  20630  chpmatply1  20637  chpmat1d  20641  chpdmat  20646  chpscmat  20647  chpscmatgsumbin  20649  chpscmatgsummon  20650  chp0mat  20651  chpidmat  20652  chmaidscmat  20653  chfacfscmulcl  20662  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmulcl  20666  chfacfpmmul0  20667  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadurid  20672  cpmidgsumm2pm  20674  cpmidpmatlem2  20676  cpmidpmatlem3  20677  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  cpmadumatpolylem1  20686  cpmadumatpolylem2  20687  cpmadumatpoly  20688  cayhamlem2  20689  chcoeffeqlem  20690  cayhamlem4  20693  cayleyhamilton0  20694  cayleyhamiltonALT  20696  cayleyhamilton1  20697  recvs  22946  fta1glem1  23925  fta1g  23927  fta1blem  23928  dchrelbas3  24963  dchrelbasd  24964  dchrzrh1  24969  dchrzrhmul  24971  dchrmulcl  24974  dchrn0  24975  dchrfi  24980  dchrghm  24981  dchrabs  24985  dchrinv  24986  dchrptlem1  24989  dchrptlem2  24990  dchrptlem3  24991  dchrsum2  24993  dchrhash  24996  sum2dchr  24999  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  lgsdchr  25080  lgseisenlem3  25102  lgseisenlem4  25103  dchrisum0flblem1  25197  dchrisum0re  25202  rdivmuldivd  29791  subofld  29816  mdetpmtr1  29889  mdetpmtr12  29891  madjusmdetlem1  29893  madjusmdetlem4  29896  mdetlap  29898  frlmpwfi  37668  isnumbasgrplem3  37675  mendlmod  37763  idomrootle  37773  idomodle  37774  2zrng0  41938  cznabel  41954  cznrng  41955  crhmsubc  42078  fldcat  42082  fldhmsubc  42084  crhmsubcALTV  42096  fldcatALTV  42100  fldhmsubcALTV  42102  mgpsumz  42141  mgpsumn  42142  evl1at0  42179  evl1at1  42180