Theorem crngring 17839

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

Syntax hints:   -> wi 4   e. wcel 1897   ` cfv 5600  CMndccmn 17478  mulGrpcmgp 17771   Ringcrg 17828   CRingccrg 17829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-iota 5564  df-fv 5608  df-cring 17831

This theorem is referenced by:  gsummgp0  17884  prdscrngd  17889  crngbinom  17897  dvdsunit  17939  unitmulclb  17941  unitabl  17944  idsrngd  18138  quscrng  18512  assa2ass  18594  sraassa  18597  rlmassa  18598  asclrhm  18614  assamulgscmlem2  18621  psrcrng  18685  psrassa  18686  mplcrng  18725  mplassa  18726  mplcoe2  18741  mplbas2  18742  mplmon2mul  18772  mplind  18773  evlslem2  18783  evlslem6  18784  evlslem3  18785  evlslem1  18786  evlseu  18787  evlsval2  18791  evlrhm  18796  evlsscasrng  18797  evlsca  18798  evlsvarsrng  18799  evlvar  18800  mpfind  18807  ply1crng  18839  ply1assa  18840  ply1coeOLD  18938  lply1binom  18948  lply1binomsc  18949  evls1rhmlem  18958  evls1gsumadd  18961  evls1gsummul  18962  evl1val  18965  evl1sca  18970  evl1scad  18971  evl1var  18972  evl1vard  18973  evls1var  18974  evls1scasrng  18975  evls1varsrng  18976  evl1subd  18978  evl1expd  18981  pf1const  18982  pf1id  18983  pf1ind  18991  evl1gsumdlem  18992  evl1gsumd  18993  evl1gsumadd  18994  evl1gsummul  18996  evl1varpw  18997  evl1scvarpw  18999  evl1scvarpwval  19000  evl1gsummon  19001  cnring  19038  zringring  19090  zring0  19097  znzrh2  19164  zncyg  19167  zndvds0  19169  znf1o  19170  zzngim  19171  znfld  19179  znchr  19181  znunit  19182  znrrg  19184  cygznlem3  19188  re0g  19228  mamuvs2  19479  matassa  19517  madetsumid  19534  madetsmelbas  19537  madetsmelbas2  19538  mat1dimcrng  19550  dmatcrng  19575  scmatcrng  19594  mdetleib2  19661  mdetf  19668  m1detdiag  19670  mdetdiaglem  19671  mdetdiag  19672  mdet1  19674  mdetrlin  19675  mdetrsca  19676  mdetrsca2  19677  mdetr0  19678  mdet0  19679  mdetrlin2  19680  mdetralt  19681  mdetero  19683  mdetmul  19696  maducoeval2  19713  maduf  19714  madutpos  19715  madugsum  19716  madurid  19717  madulid  19718  marep01ma  19733  smadiadetlem0  19734  smadiadetlem1a  19736  smadiadetlem3lem2  19740  smadiadetlem3  19741  smadiadetlem4  19742  smadiadet  19743  smadiadetglem1  19744  smadiadetglem2  19745  smadiadetg  19746  matinv  19750  matunit  19751  slesolinv  19753  slesolinvbi  19754  slesolex  19755  cramerimplem1  19756  cramerimplem2  19757  cramerimplem3  19758  cramerimp  19759  cramer  19764  mat2pmatmul  19803  mat2pmatmhm  19805  mat2pmatrhm  19806  mat2pmatlin  19807  m2cpmmhm  19817  m2cpmrhm  19818  m2pmfzgsumcl  19820  m2cpmrngiso  19830  monmatcollpw  19851  pmatcollpwlem  19852  pmatcollpw  19853  pmatcollpwfi  19854  pmatcollpw3fi1lem2  19859  pmatcollpwscmat  19863  monmat2matmon  19896  pm2mp  19897  chpmatply1  19904  chpmat1d  19908  chpdmat  19913  chpscmat  19914  chpscmatgsumbin  19916  chpscmatgsummon  19917  chp0mat  19918  chpidmat  19919  chmaidscmat  19920  chfacfscmulcl  19929  chfacfscmul0  19930  chfacfscmulgsum  19932  chfacfpmmulcl  19933  chfacfpmmul0  19934  chfacfpmmulgsum  19936  chfacfpmmulgsum2  19937  cayhamlem1  19938  cpmadurid  19939  cpmidgsumm2pm  19941  cpmidpmatlem2  19943  cpmidpmatlem3  19944  cpmadugsumlemB  19946  cpmadugsumlemC  19947  cpmadugsumlemF  19948  cpmadugsumfi  19949  cpmidgsum2  19951  cpmadumatpolylem1  19953  cpmadumatpolylem2  19954  cpmadumatpoly  19955  cayhamlem2  19956  chcoeffeqlem  19957  cayhamlem4  19960  cayleyhamilton0  19961  cayleyhamiltonALT  19963  cayleyhamilton1  19964  fta1glem1  23164  fta1g  23166  fta1blem  23167  dchrelbas3  24214  dchrelbasd  24215  dchrzrh1  24220  dchrzrhmul  24222  dchrmulcl  24225  dchrn0  24226  dchrfi  24231  dchrghm  24232  dchrabs  24236  dchrinv  24237  dchrptlem1  24240  dchrptlem2  24241  dchrptlem3  24242  dchrsum2  24244  dchrhash  24247  sum2dchr  24250  lgsqrlem1  24317  lgsqrlem2  24318  lgsqrlem3  24319  lgsqrlem4  24320  lgsdchr  24324  lgseisenlem3  24327  lgseisenlem4  24328  dchrisum0flblem1  24394  dchrisum0re  24399  rdivmuldivd  28602  subofld  28627  mdetpmtr1  28697  mdetpmtr12  28699  madjusmdetlem1  28701  madjusmdetlem4  28704  mdetlap  28706  frlmpwfi  36000  isnumbasgrplem3  36008  mendlmod  36103  idomrootle  36113  idomodle  36114  2zrng0  40210  cznabel  40228  cznrng  40229  crhmsubc  40352  fldcat  40356  fldhmsubc  40358  crhmsubcALTV  40371  fldcatALTV  40375  fldhmsubcALTV  40377  mgpsumz  40416  mgpsumn  40417  evl1at0  40455  evl1at1  40456