Theorem crngring 17734

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 2428	. . 3 |- (mulGrp ` R ) = (mulGrp ` R )
2	1	iscrng 17730	. 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 1872   ` cfv 5544  CMndccmn 17373  mulGrpcmgp 17666   Ringcrg 17723   CRingccrg 17724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-iota 5508  df-fv 5552  df-cring 17726

This theorem is referenced by:  gsummgp0  17779  prdscrngd  17784  crngbinom  17792  dvdsunit  17834  unitmulclb  17836  unitabl  17839  idsrngd  18033  quscrng  18407  assa2ass  18489  sraassa  18492  rlmassa  18493  asclrhm  18509  assamulgscmlem2  18516  psrcrng  18580  psrassa  18581  mplcrng  18620  mplassa  18621  mplcoe2  18636  mplbas2  18637  mplmon2mul  18667  mplind  18668  evlslem2  18678  evlslem6  18679  evlslem3  18680  evlslem1  18681  evlseu  18682  evlsval2  18686  evlrhm  18691  evlsscasrng  18692  evlsca  18693  evlsvarsrng  18694  evlvar  18695  mpfind  18702  ply1crng  18734  ply1assa  18735  ply1coeOLD  18833  lply1binom  18843  lply1binomsc  18844  evls1rhmlem  18853  evls1gsumadd  18856  evls1gsummul  18857  evl1val  18860  evl1sca  18865  evl1scad  18866  evl1var  18867  evl1vard  18868  evls1var  18869  evls1scasrng  18870  evls1varsrng  18871  evl1subd  18873  evl1expd  18876  pf1const  18877  pf1id  18878  pf1ind  18886  evl1gsumdlem  18887  evl1gsumd  18888  evl1gsumadd  18889  evl1gsummul  18891  evl1varpw  18892  evl1scvarpw  18894  evl1scvarpwval  18895  evl1gsummon  18896  cnring  18933  zringring  18984  zring0  18991  znzrh2  19058  zncyg  19061  zndvds0  19063  znf1o  19064  zzngim  19065  znfld  19073  znchr  19075  znunit  19076  znrrg  19078  cygznlem3  19082  re0g  19122  mamuvs2  19373  matassa  19411  madetsumid  19428  madetsmelbas  19431  madetsmelbas2  19432  mat1dimcrng  19444  dmatcrng  19469  scmatcrng  19488  mdetleib2  19555  mdetf  19562  m1detdiag  19564  mdetdiaglem  19565  mdetdiag  19566  mdet1  19568  mdetrlin  19569  mdetrsca  19570  mdetrsca2  19571  mdetr0  19572  mdet0  19573  mdetrlin2  19574  mdetralt  19575  mdetero  19577  mdetmul  19590  maducoeval2  19607  maduf  19608  madutpos  19609  madugsum  19610  madurid  19611  madulid  19612  marep01ma  19627  smadiadetlem0  19628  smadiadetlem1a  19630  smadiadetlem3lem2  19634  smadiadetlem3  19635  smadiadetlem4  19636  smadiadet  19637  smadiadetglem1  19638  smadiadetglem2  19639  smadiadetg  19640  matinv  19644  matunit  19645  slesolinv  19647  slesolinvbi  19648  slesolex  19649  cramerimplem1  19650  cramerimplem2  19651  cramerimplem3  19652  cramerimp  19653  cramer  19658  mat2pmatmul  19697  mat2pmatmhm  19699  mat2pmatrhm  19700  mat2pmatlin  19701  m2cpmmhm  19711  m2cpmrhm  19712  m2pmfzgsumcl  19714  m2cpmrngiso  19724  monmatcollpw  19745  pmatcollpwlem  19746  pmatcollpw  19747  pmatcollpwfi  19748  pmatcollpw3fi1lem2  19753  pmatcollpwscmat  19757  monmat2matmon  19790  pm2mp  19791  chpmatply1  19798  chpmat1d  19802  chpdmat  19807  chpscmat  19808  chpscmatgsumbin  19810  chpscmatgsummon  19811  chp0mat  19812  chpidmat  19813  chmaidscmat  19814  chfacfscmulcl  19823  chfacfscmul0  19824  chfacfscmulgsum  19826  chfacfpmmulcl  19827  chfacfpmmul0  19828  chfacfpmmulgsum  19830  chfacfpmmulgsum2  19831  cayhamlem1  19832  cpmadurid  19833  cpmidgsumm2pm  19835  cpmidpmatlem2  19837  cpmidpmatlem3  19838  cpmadugsumlemB  19840  cpmadugsumlemC  19841  cpmadugsumlemF  19842  cpmadugsumfi  19843  cpmidgsum2  19845  cpmadumatpolylem1  19847  cpmadumatpolylem2  19848  cpmadumatpoly  19849  cayhamlem2  19850  chcoeffeqlem  19851  cayhamlem4  19854  cayleyhamilton0  19855  cayleyhamiltonALT  19857  cayleyhamilton1  19858  fta1glem1  23058  fta1g  23060  fta1blem  23061  dchrelbas3  24108  dchrelbasd  24109  dchrzrh1  24114  dchrzrhmul  24116  dchrmulcl  24119  dchrn0  24120  dchrfi  24125  dchrghm  24126  dchrabs  24130  dchrinv  24131  dchrptlem1  24134  dchrptlem2  24135  dchrptlem3  24136  dchrsum2  24138  dchrhash  24141  sum2dchr  24144  lgsqrlem1  24211  lgsqrlem2  24212  lgsqrlem3  24213  lgsqrlem4  24214  lgsdchr  24218  lgseisenlem3  24221  lgseisenlem4  24222  dchrisum0flblem1  24288  dchrisum0re  24293  rdivmuldivd  28506  subofld  28531  mdetpmtr1  28601  mdetpmtr12  28603  madjusmdetlem1  28605  madjusmdetlem4  28608  mdetlap  28610  frlmpwfi  35869  isnumbasgrplem3  35877  mendlmod  35972  idomrootle  35982  idomodle  35983  2zrng0  39539  cznabel  39557  cznrng  39558  crhmsubc  39681  fldcat  39685  fldhmsubc  39687  crhmsubcALTV  39700  fldcatALTV  39704  fldhmsubcALTV  39706  mgpsumz  39747  mgpsumn  39748  evl1at0  39786  evl1at1  39787