Theorem crngring 17187

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 2443	. . 3 |- (mulGrp ` R ) = (mulGrp ` R )
2	1	iscrng 17183	. 2 |- ( R e. CRing <-> ( R e. Ring /\ (mulGrp ` R ) e. CMnd ) )
3	2	simplbi 460	1 |- ( R e. CRing -> R e. Ring )

Syntax hints:   -> wi 4   e. wcel 1804   ` cfv 5578  CMndccmn 16776  mulGrpcmgp 17119   Ringcrg 17176   CRingccrg 17177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-cring 17179

This theorem is referenced by:  gsummgp0  17234  prdscrngd  17240  crngbinom  17248  dvdsunit  17290  unitmulclb  17292  unitabl  17295  idsrngd  17489  quscrng  17866  assa2ass  17949  sraassa  17952  rlmassa  17953  asclrhm  17969  assamulgscmlem2  17976  psrcrng  18046  psrassa  18047  mplcrng  18093  mplassa  18094  mplcoe2  18110  mplcoe2OLD  18111  mplbas2  18112  mplbas2OLD  18113  mplmon2mul  18144  mplind  18145  evlslem2  18158  evlslem6  18159  evlslem6OLD  18160  evlslem3  18161  evlslem1  18162  evlseu  18163  evlsval2  18167  evlrhm  18172  evlsscasrng  18173  evlsca  18174  evlsvarsrng  18175  evlvar  18176  mpfind  18183  ply1crng  18215  ply1assa  18216  ply1coeOLD  18316  lply1binom  18326  lply1binomsc  18327  evls1rhmlem  18336  evls1gsumadd  18339  evls1gsummul  18340  evl1val  18343  evl1sca  18348  evl1scad  18349  evl1var  18350  evl1vard  18351  evls1var  18352  evls1scasrng  18353  evls1varsrng  18354  evl1subd  18356  evl1expd  18359  pf1const  18360  pf1id  18361  pf1ind  18369  evl1gsumdlem  18370  evl1gsumd  18371  evl1gsumadd  18372  evl1gsummul  18374  evl1varpw  18375  evl1scvarpw  18377  evl1scvarpwval  18378  evl1gsummon  18379  cnring  18418  zringring  18469  zring0  18476  zrng0  18482  znzrh2  18561  zncyg  18564  zndvds0  18566  znf1o  18567  zzngim  18568  znfld  18576  znchr  18578  znunit  18579  znrrg  18581  cygznlem3  18585  re0g  18625  mamuvs2  18885  matassa  18923  madetsumid  18940  madetsmelbas  18943  madetsmelbas2  18944  mat1dimcrng  18956  dmatcrng  18981  scmatcrng  19000  mdetleib2  19067  mdetf  19074  m1detdiag  19076  mdetdiaglem  19077  mdetdiag  19078  mdet1  19080  mdetrlin  19081  mdetrsca  19082  mdetrsca2  19083  mdetr0  19084  mdet0  19085  mdetrlin2  19086  mdetralt  19087  mdetero  19089  mdetmul  19102  maducoeval2  19119  maduf  19120  madutpos  19121  madugsum  19122  madurid  19123  madulid  19124  marep01ma  19139  smadiadetlem0  19140  smadiadetlem1a  19142  smadiadetlem3lem2  19146  smadiadetlem3  19147  smadiadetlem4  19148  smadiadet  19149  smadiadetglem1  19150  smadiadetglem2  19151  smadiadetg  19152  matinv  19156  matunit  19157  slesolinv  19159  slesolinvbi  19160  slesolex  19161  cramerimplem1  19162  cramerimplem2  19163  cramerimplem3  19164  cramerimp  19165  cramer  19170  mat2pmatmul  19209  mat2pmatmhm  19211  mat2pmatrhm  19212  mat2pmatlin  19213  m2cpmmhm  19223  m2cpmrhm  19224  m2pmfzgsumcl  19226  m2cpmrngiso  19236  monmatcollpw  19257  pmatcollpwlem  19258  pmatcollpw  19259  pmatcollpwfi  19260  pmatcollpw3fi1lem2  19265  pmatcollpwscmat  19269  monmat2matmon  19302  pm2mp  19303  chpmatply1  19310  chpmat1d  19314  chpdmat  19319  chpscmat  19320  chpscmatgsumbin  19322  chpscmatgsummon  19323  chp0mat  19324  chpidmat  19325  chmaidscmat  19326  chfacfscmulcl  19335  chfacfscmul0  19336  chfacfscmulgsum  19338  chfacfpmmulcl  19339  chfacfpmmul0  19340  chfacfpmmulgsum  19342  chfacfpmmulgsum2  19343  cayhamlem1  19344  cpmadurid  19345  cpmidgsumm2pm  19347  cpmidpmatlem2  19349  cpmidpmatlem3  19350  cpmadugsumlemB  19352  cpmadugsumlemC  19353  cpmadugsumlemF  19354  cpmadugsumfi  19355  cpmidgsum2  19357  cpmadumatpolylem1  19359  cpmadumatpolylem2  19360  cpmadumatpoly  19361  cayhamlem2  19362  chcoeffeqlem  19363  cayhamlem4  19366  cayleyhamilton0  19367  cayleyhamiltonALT  19369  cayleyhamilton1  19370  fta1glem1  22543  fta1g  22545  fta1blem  22546  dchrelbas3  23489  dchrelbasd  23490  dchrzrh1  23495  dchrzrhmul  23497  dchrmulcl  23500  dchrn0  23501  dchrfi  23506  dchrghm  23507  dchrabs  23511  dchrinv  23512  dchrptlem1  23515  dchrptlem2  23516  dchrptlem3  23517  dchrsum2  23519  dchrhash  23522  sum2dchr  23525  lgsqrlem1  23592  lgsqrlem2  23593  lgsqrlem3  23594  lgsqrlem4  23595  lgsdchr  23599  lgseisenlem3  23602  lgseisenlem4  23603  dchrisum0flblem1  23669  dchrisum0re  23674  rdivmuldivd  27758  subofld  27783  frlmpwfi  31021  isnumbasgrplem3  31029  mendlmod  31118  idomrootle  31128  idomodle  31129  2zrng0  32454  cznabel  32472  cznrng  32473  crhmsubc  32619  fldcat  32623  fldhmsubc  32625  crhmsubcOLD  32638  fldcatOLD  32642  fldhmsubcOLD  32644  mgpsumz  32685  mgpsumn  32686  evl1at0  32726  evl1at1  32727