Theorem crngring 20158

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 2731	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	iscrng 20153	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
3	2	simplbi 497	1 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6476  CMndccmn 19687  mulGrpcmgp 20053  Ringcrg 20146  CRingccrg 20147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-cring 20149

This theorem is referenced by:  crngringd  20159  gsummgp0  20231  prdscrngd  20235  crngbinom  20248  dvdsunit  20292  unitmulclb  20294  unitabl  20297  rdivmuldivd  20326  crhmsubc  20592  fldcat  20693  fldhmsubc  20695  idsrngd  20766  subofld  20787  rmodislmod  20858  quscrng  21215  cnring  21322  zringring  21381  zring0  21390  znzrh2  21477  zncyg  21480  zndvds0  21482  znf1o  21483  zzngim  21484  znfld  21492  znchr  21494  znunit  21495  znrrg  21497  cygznlem3  21501  freshmansdream  21506  re0g  21544  sraassa  21801  sraassaOLD  21802  rlmassa  21803  psrcrng  21904  mplcrng  21953  mplassa  21954  mplcoe2  21971  mplbas2  21972  mplmon2mul  21999  mplind  22000  evlslem2  22009  evlslem3  22010  evlslem6  22011  evlseu  22013  evlsval2  22017  evlsgsumadd  22021  evlsgsummul  22022  evlrhm  22026  evlsscasrng  22027  evlsca  22028  evlsvarsrng  22029  evlvar  22030  mpfind  22037  ply1crng  22106  ply1assa  22107  ply1chr  22216  lply1binom  22220  lply1binomsc  22221  evls1rhmlem  22231  evls1gsumadd  22234  evls1gsummul  22235  evl1val  22239  evl1sca  22244  evl1scad  22245  evl1var  22246  evl1vard  22247  evls1var  22248  evls1scasrng  22249  evls1varsrng  22250  evl1subd  22252  evl1expd  22255  pf1const  22256  pf1id  22257  pf1ind  22265  evl1gsumdlem  22266  evl1gsumd  22267  evl1gsumadd  22268  evl1gsummul  22270  evl1varpw  22271  evl1scvarpw  22273  evl1scvarpwval  22274  evl1gsummon  22275  evls1vsca  22283  mamuvs2  22316  matassa  22354  madetsumid  22371  madetsmelbas  22374  madetsmelbas2  22375  mat1dimcrng  22387  dmatcrng  22412  scmatcrng  22431  mdetleib2  22498  mdetf  22505  m1detdiag  22507  mdetdiaglem  22508  mdetdiag  22509  mdet1  22511  mdetrlin  22512  mdetrsca2  22514  mdetr0  22515  mdet0  22516  mdetrlin2  22517  mdetralt  22518  mdetero  22520  mdetmul  22533  maducoeval2  22550  maduf  22551  madutpos  22552  madugsum  22553  madurid  22554  madulid  22555  marep01ma  22570  smadiadetlem0  22571  smadiadetlem1a  22573  smadiadetlem3lem2  22577  smadiadetlem3  22578  smadiadetlem4  22579  smadiadet  22580  smadiadetglem1  22581  smadiadetglem2  22582  smadiadetg  22583  matinv  22587  matunit  22588  slesolinv  22590  slesolinvbi  22591  slesolex  22592  cramerimplem1  22593  cramerimplem2  22594  cramerimplem3  22595  cramerimp  22596  cramer  22601  mat2pmatmul  22641  mat2pmatmhm  22643  mat2pmatrhm  22644  mat2pmatlin  22645  m2cpmmhm  22655  m2cpmrhm  22656  m2pmfzgsumcl  22658  m2cpmrngiso  22668  monmatcollpw  22689  pmatcollpwlem  22690  pmatcollpw  22691  pmatcollpwfi  22692  pmatcollpw3fi1lem2  22697  pmatcollpwscmat  22701  monmat2matmon  22734  pm2mp  22735  chpmatply1  22742  chpmat1d  22746  chpdmat  22751  chpscmat  22752  chpscmatgsumbin  22754  chpscmatgsummon  22755  chp0mat  22756  chpidmat  22757  chmaidscmat  22758  chfacfscmulcl  22767  chfacfscmul0  22768  chfacfscmulgsum  22770  chfacfpmmulcl  22771  chfacfpmmul0  22772  chfacfpmmulgsum  22774  chfacfpmmulgsum2  22775  cayhamlem1  22776  cpmadurid  22777  cpmidgsumm2pm  22779  cpmidpmatlem2  22781  cpmidpmatlem3  22782  cpmadugsumlemB  22784  cpmadugsumlemC  22785  cpmadugsumlemF  22786  cpmadugsumfi  22787  cpmidgsum2  22789  cpmadumatpolylem1  22791  cpmadumatpolylem2  22792  cpmadumatpoly  22793  cayhamlem2  22794  chcoeffeqlem  22795  cayhamlem4  22798  cayleyhamilton0  22799  cayleyhamiltonALT  22801  cayleyhamilton1  22802  fta1glem1  26095  fta1g  26097  fta1blem  26098  idomrootle  26100  dchrelbas3  27171  dchrelbasd  27172  dchrzrh1  27177  dchrzrhmul  27179  dchrmulcl  27182  dchrn0  27183  dchrfi  27188  dchrghm  27189  dchrabs  27193  dchrinv  27194  dchrptlem1  27197  dchrptlem2  27198  dchrptlem3  27199  dchrsum2  27201  dchrhash  27204  sum2dchr  27207  lgsqrlem1  27279  lgsqrlem2  27280  lgsqrlem3  27281  lgsqrlem4  27282  lgsdchr  27288  lgseisenlem3  27310  lgseisenlem4  27311  dchrisum0flblem1  27441  dchrisum0re  27446  unitprodclb  33346  ringlsmss1  33353  isprmidlc  33404  prmidl0  33407  qsidomlem1  33409  qsidomlem2  33410  crngmxidl  33426  mxidlprm  33427  idlsrgmulrss1  33468  mdetpmtr1  33828  mdetpmtr12  33830  madjusmdetlem1  33832  madjusmdetlem4  33835  mdetlap  33837  zarcls1  33874  zarclsint  33877  zarclssn  33878  zartopn  33880  zart0  33884  zarcmplem  33886  rspectps  33888  aks6d1c1p2  42142  aks6d1c1p7  42146  aks6d1c1p6  42147  aks6d1c1  42149  hashscontpowcl  42153  hashscontpow  42155  aks6d1c4  42157  aks6d1c2lem3  42159  aks6d1c2  42163  aks6d1c5lem1  42169  aks6d1c5lem3  42170  aks6d1c6lem1  42203  aks6d1c6lem3  42205  aks6d1c6lem5  42210  aks6d1c7lem1  42213  aks5lem1  42219  aks5lem2  42220  aks5lem5a  42224  frlmpwfi  43131  isnumbasgrplem3  43138  mendlmod  43222  idomodle  43224  2zrng0  48275  cznabel  48291  cznrng  48292  crhmsubcALTV  48358  fldcatALTV  48362  fldhmsubcALTV  48364  mgpsumz  48393  mgpsumn  48394  evl1at0  48423  evl1at1  48424