Theorem crngring 17726

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

Syntax hints:   -> wi 4   e. wcel 1870   ` cfv 5601  CMndccmn 17365  mulGrpcmgp 17658   Ringcrg 17715   CRingccrg 17716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-cring 17718

This theorem is referenced by:  gsummgp0  17771  prdscrngd  17776  crngbinom  17784  dvdsunit  17826  unitmulclb  17828  unitabl  17831  idsrngd  18025  quscrng  18399  assa2ass  18481  sraassa  18484  rlmassa  18485  asclrhm  18501  assamulgscmlem2  18508  psrcrng  18572  psrassa  18573  mplcrng  18612  mplassa  18613  mplcoe2  18628  mplbas2  18629  mplmon2mul  18659  mplind  18660  evlslem2  18670  evlslem6  18671  evlslem3  18672  evlslem1  18673  evlseu  18674  evlsval2  18678  evlrhm  18683  evlsscasrng  18684  evlsca  18685  evlsvarsrng  18686  evlvar  18687  mpfind  18694  ply1crng  18726  ply1assa  18727  ply1coeOLD  18825  lply1binom  18835  lply1binomsc  18836  evls1rhmlem  18845  evls1gsumadd  18848  evls1gsummul  18849  evl1val  18852  evl1sca  18857  evl1scad  18858  evl1var  18859  evl1vard  18860  evls1var  18861  evls1scasrng  18862  evls1varsrng  18863  evl1subd  18865  evl1expd  18868  pf1const  18869  pf1id  18870  pf1ind  18878  evl1gsumdlem  18879  evl1gsumd  18880  evl1gsumadd  18881  evl1gsummul  18883  evl1varpw  18884  evl1scvarpw  18886  evl1scvarpwval  18887  evl1gsummon  18888  cnring  18925  zringring  18976  zring0  18983  znzrh2  19047  zncyg  19050  zndvds0  19052  znf1o  19053  zzngim  19054  znfld  19062  znchr  19064  znunit  19065  znrrg  19067  cygznlem3  19071  re0g  19111  mamuvs2  19362  matassa  19400  madetsumid  19417  madetsmelbas  19420  madetsmelbas2  19421  mat1dimcrng  19433  dmatcrng  19458  scmatcrng  19477  mdetleib2  19544  mdetf  19551  m1detdiag  19553  mdetdiaglem  19554  mdetdiag  19555  mdet1  19557  mdetrlin  19558  mdetrsca  19559  mdetrsca2  19560  mdetr0  19561  mdet0  19562  mdetrlin2  19563  mdetralt  19564  mdetero  19566  mdetmul  19579  maducoeval2  19596  maduf  19597  madutpos  19598  madugsum  19599  madurid  19600  madulid  19601  marep01ma  19616  smadiadetlem0  19617  smadiadetlem1a  19619  smadiadetlem3lem2  19623  smadiadetlem3  19624  smadiadetlem4  19625  smadiadet  19626  smadiadetglem1  19627  smadiadetglem2  19628  smadiadetg  19629  matinv  19633  matunit  19634  slesolinv  19636  slesolinvbi  19637  slesolex  19638  cramerimplem1  19639  cramerimplem2  19640  cramerimplem3  19641  cramerimp  19642  cramer  19647  mat2pmatmul  19686  mat2pmatmhm  19688  mat2pmatrhm  19689  mat2pmatlin  19690  m2cpmmhm  19700  m2cpmrhm  19701  m2pmfzgsumcl  19703  m2cpmrngiso  19713  monmatcollpw  19734  pmatcollpwlem  19735  pmatcollpw  19736  pmatcollpwfi  19737  pmatcollpw3fi1lem2  19742  pmatcollpwscmat  19746  monmat2matmon  19779  pm2mp  19780  chpmatply1  19787  chpmat1d  19791  chpdmat  19796  chpscmat  19797  chpscmatgsumbin  19799  chpscmatgsummon  19800  chp0mat  19801  chpidmat  19802  chmaidscmat  19803  chfacfscmulcl  19812  chfacfscmul0  19813  chfacfscmulgsum  19815  chfacfpmmulcl  19816  chfacfpmmul0  19817  chfacfpmmulgsum  19819  chfacfpmmulgsum2  19820  cayhamlem1  19821  cpmadurid  19822  cpmidgsumm2pm  19824  cpmidpmatlem2  19826  cpmidpmatlem3  19827  cpmadugsumlemB  19829  cpmadugsumlemC  19830  cpmadugsumlemF  19831  cpmadugsumfi  19832  cpmidgsum2  19834  cpmadumatpolylem1  19836  cpmadumatpolylem2  19837  cpmadumatpoly  19838  cayhamlem2  19839  chcoeffeqlem  19840  cayhamlem4  19843  cayleyhamilton0  19844  cayleyhamiltonALT  19846  cayleyhamilton1  19847  fta1glem1  22991  fta1g  22993  fta1blem  22994  dchrelbas3  24029  dchrelbasd  24030  dchrzrh1  24035  dchrzrhmul  24037  dchrmulcl  24040  dchrn0  24041  dchrfi  24046  dchrghm  24047  dchrabs  24051  dchrinv  24052  dchrptlem1  24055  dchrptlem2  24056  dchrptlem3  24057  dchrsum2  24059  dchrhash  24062  sum2dchr  24065  lgsqrlem1  24132  lgsqrlem2  24133  lgsqrlem3  24134  lgsqrlem4  24135  lgsdchr  24139  lgseisenlem3  24142  lgseisenlem4  24143  dchrisum0flblem1  24209  dchrisum0re  24214  rdivmuldivd  28393  subofld  28418  mdetpmtr1  28488  mdetpmtr12  28490  madjusmdetlem1  28492  madjusmdetlem4  28495  mdetlap  28497  frlmpwfi  35661  isnumbasgrplem3  35669  mendlmod  35757  idomrootle  35767  idomodle  35768  2zrng0  38695  cznabel  38713  cznrng  38714  crhmsubc  38837  fldcat  38841  fldhmsubc  38843  crhmsubcALTV  38856  fldcatALTV  38860  fldhmsubcALTV  38862  mgpsumz  38903  mgpsumn  38904  evl1at0  38942  evl1at1  38943