Theorem crngring 20070

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

Assertion

Ref	Expression
crngring	⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Proof of Theorem crngring

Step	Hyp	Ref	Expression
1		eqid 2732	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	iscrng 20065	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
3	2	simplbi 498	1 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6543  CMndccmn 19650  mulGrpcmgp 19989  Ringcrg 20058  CRingccrg 20059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-cring 20061

This theorem is referenced by:  crngringd  20071  gsummgp0  20134  prdscrngd  20139  crngbinom  20152  dvdsunit  20197  unitmulclb  20199  unitabl  20202  rdivmuldivd  20231  idsrngd  20474  rmodislmod  20545  rmodislmodOLD  20546  quscrng  20884  cnring  20973  zringring  21026  zring0  21034  znzrh2  21107  zncyg  21110  zndvds0  21112  znf1o  21113  zzngim  21114  znfld  21122  znchr  21124  znunit  21125  znrrg  21127  cygznlem3  21131  re0g  21171  sraassa  21429  sraassaOLD  21430  rlmassa  21431  psrcrng  21539  mplcrng  21586  mplassa  21587  mplcoe2  21602  mplbas2  21603  mplmon2mul  21636  mplind  21637  evlslem2  21648  evlslem3  21649  evlslem6  21650  evlseu  21652  evlsval2  21656  evlsgsumadd  21660  evlsgsummul  21661  evlrhm  21665  evlsscasrng  21666  evlsca  21667  evlsvarsrng  21668  evlvar  21669  mpfind  21676  ply1crng  21728  ply1assa  21729  lply1binom  21837  lply1binomsc  21838  evls1rhmlem  21847  evls1gsumadd  21850  evls1gsummul  21851  evl1val  21855  evl1sca  21860  evl1scad  21861  evl1var  21862  evl1vard  21863  evls1var  21864  evls1scasrng  21865  evls1varsrng  21866  evl1subd  21868  evl1expd  21871  pf1const  21872  pf1id  21873  pf1ind  21881  evl1gsumdlem  21882  evl1gsumd  21883  evl1gsumadd  21884  evl1gsummul  21886  evl1varpw  21887  evl1scvarpw  21889  evl1scvarpwval  21890  evl1gsummon  21891  mamuvs2  21913  matassa  21953  madetsumid  21970  madetsmelbas  21973  madetsmelbas2  21974  mat1dimcrng  21986  dmatcrng  22011  scmatcrng  22030  mdetleib2  22097  mdetf  22104  m1detdiag  22106  mdetdiaglem  22107  mdetdiag  22108  mdet1  22110  mdetrlin  22111  mdetrsca2  22113  mdetr0  22114  mdet0  22115  mdetrlin2  22116  mdetralt  22117  mdetero  22119  mdetmul  22132  maducoeval2  22149  maduf  22150  madutpos  22151  madugsum  22152  madurid  22153  madulid  22154  marep01ma  22169  smadiadetlem0  22170  smadiadetlem1a  22172  smadiadetlem3lem2  22176  smadiadetlem3  22177  smadiadetlem4  22178  smadiadet  22179  smadiadetglem1  22180  smadiadetglem2  22181  smadiadetg  22182  matinv  22186  matunit  22187  slesolinv  22189  slesolinvbi  22190  slesolex  22191  cramerimplem1  22192  cramerimplem2  22193  cramerimplem3  22194  cramerimp  22195  cramer  22200  mat2pmatmul  22240  mat2pmatmhm  22242  mat2pmatrhm  22243  mat2pmatlin  22244  m2cpmmhm  22254  m2cpmrhm  22255  m2pmfzgsumcl  22257  m2cpmrngiso  22267  monmatcollpw  22288  pmatcollpwlem  22289  pmatcollpw  22290  pmatcollpwfi  22291  pmatcollpw3fi1lem2  22296  pmatcollpwscmat  22300  monmat2matmon  22333  pm2mp  22334  chpmatply1  22341  chpmat1d  22345  chpdmat  22350  chpscmat  22351  chpscmatgsumbin  22353  chpscmatgsummon  22354  chp0mat  22355  chpidmat  22356  chmaidscmat  22357  chfacfscmulcl  22366  chfacfscmul0  22367  chfacfscmulgsum  22369  chfacfpmmulcl  22370  chfacfpmmul0  22371  chfacfpmmulgsum  22373  chfacfpmmulgsum2  22374  cayhamlem1  22375  cpmadurid  22376  cpmidgsumm2pm  22378  cpmidpmatlem2  22380  cpmidpmatlem3  22381  cpmadugsumlemB  22383  cpmadugsumlemC  22384  cpmadugsumlemF  22385  cpmadugsumfi  22386  cpmidgsum2  22388  cpmadumatpolylem1  22390  cpmadumatpolylem2  22391  cpmadumatpoly  22392  cayhamlem2  22393  chcoeffeqlem  22394  cayhamlem4  22397  cayleyhamilton0  22398  cayleyhamiltonALT  22400  cayleyhamilton1  22401  recvsOLD  24670  fta1glem1  25690  fta1g  25692  fta1blem  25693  dchrelbas3  26748  dchrelbasd  26749  dchrzrh1  26754  dchrzrhmul  26756  dchrmulcl  26759  dchrn0  26760  dchrfi  26765  dchrghm  26766  dchrabs  26770  dchrinv  26771  dchrptlem1  26774  dchrptlem2  26775  dchrptlem3  26776  dchrsum2  26778  dchrhash  26781  sum2dchr  26784  lgsqrlem1  26856  lgsqrlem2  26857  lgsqrlem3  26858  lgsqrlem4  26859  lgsdchr  26865  lgseisenlem3  26887  lgseisenlem4  26888  dchrisum0flblem1  27018  dchrisum0re  27023  freshmansdream  32422  subofld  32475  ringlsmss1  32551  isprmidlc  32611  prmidl0  32614  qsidomlem1  32616  qsidomlem2  32617  crngmxidl  32630  mxidlprm  32631  idlsrgmulrss1  32670  evls1vsca  32695  ply1chr  32706  mdetpmtr1  32872  mdetpmtr12  32874  madjusmdetlem1  32876  madjusmdetlem4  32879  mdetlap  32881  zarcls1  32918  zarclsint  32921  zarclssn  32922  zartopn  32924  zart0  32928  zarcmplem  32930  rspectps  32932  selvcllem5  41236  frlmpwfi  41922  isnumbasgrplem3  41929  mendlmod  42017  idomrootle  42019  idomodle  42020  2zrng0  46915  cznabel  46931  cznrng  46932  crhmsubc  47055  fldcat  47059  fldhmsubc  47061  crhmsubcALTV  47073  fldcatALTV  47077  fldhmsubcALTV  47079  mgpsumz  47117  mgpsumn  47118  evl1at0  47150  evl1at1  47151