Theorem crngring 20329

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

Syntax hints:   → wi 4   ∈ wcel 2149  ‘cfv 6539  CMndccmn 19852  mulGrpcmgp 20218  Ringcrg 20317  CRingccrg 20318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6495  df-fv 6547  df-cring 20320

This theorem is referenced by:  crngringd  20330  gsummgp0  20401  prdscrngd  20405  crngbinom  20419  dvdsunit  20463  unitmulclb  20465  unitabl  20468  rdivmuldivd  20497  crhmsubc  20769  fldcat  20866  fldhmsubc  20868  idsrngd  20939  subofld  20960  rmodislmod  21031  df2idl2crng  21394  quscrng  21396  isprmidlc  21445  prmidl0  21449  qsidomlem1  21451  qsidomlem2  21452  prmidlsubm  21458  cnring  21515  zringring  21570  zring0  21579  znzrh2  21666  zncyg  21669  zndvds0  21671  znf1o  21672  zzngim  21673  znfld  21681  znchr  21683  znunit  21684  znrrg  21686  cygznlem3  21690  freshmansdream  21695  re0g  21733  sraassa  21990  rlmassa  21991  psrcrng  22092  mplcrng  22141  mplassa  22142  mplcoe2  22163  mplbas2  22164  mplmon2mul  22191  mplind  22192  evlslem2  22201  evlslem3  22202  evlslem6  22203  evlseu  22205  evlsval2  22209  evlsgsumadd  22218  evlsgsummul  22219  evlrhm  22223  evlsscasrng  22227  evlsca  22228  evlsvarsrng  22229  evlvar  22230  mpfind  22237  ply1crng  22329  ply1assa  22330  ply1chr  22437  lply1binom  22441  lply1binomsc  22442  evls1rhmlem  22452  evls1gsumadd  22455  evls1gsummul  22456  evl1val  22460  evl1sca  22465  evl1scad  22466  evl1var  22467  evl1vard  22468  evls1var  22469  evls1scasrng  22470  evls1varsrng  22471  evl1subd  22473  evl1expd  22476  pf1const  22477  pf1id  22478  pf1ind  22486  evl1gsumdlem  22487  evl1gsumd  22488  evl1gsumadd  22489  evl1gsummul  22491  evl1varpw  22492  evl1scvarpw  22494  evl1scvarpwval  22495  evl1gsummon  22496  evls1vsca  22504  mamuvs2  22534  matassa  22572  madetsumid  22589  madetsmelbas  22592  madetsmelbas2  22593  mat1dimcrng  22605  dmatcrng  22630  scmatcrng  22649  mdetleib2  22716  mdetf  22723  m1detdiag  22725  mdetdiaglem  22726  mdetdiag  22727  mdet1  22729  mdetrlin  22730  mdetrsca2  22732  mdetr0  22733  mdet0  22734  mdetrlin2  22735  mdetralt  22736  mdetero  22738  mdetmul  22751  maducoeval2  22768  maduf  22769  madutpos  22770  madugsum  22771  madurid  22772  madulid  22773  marep01ma  22788  smadiadetlem0  22789  smadiadetlem1a  22791  smadiadetlem3lem2  22795  smadiadetlem3  22796  smadiadetlem4  22797  smadiadet  22798  smadiadetglem1  22799  smadiadetglem2  22800  smadiadetg  22801  matinv  22805  matunit  22806  slesolinv  22808  slesolinvbi  22809  slesolex  22810  cramerimplem1  22811  cramerimplem2  22812  cramerimplem3  22813  cramerimp  22814  cramer  22819  mat2pmatmul  22859  mat2pmatmhm  22861  mat2pmatrhm  22862  mat2pmatlin  22863  m2cpmmhm  22873  m2cpmrhm  22874  m2pmfzgsumcl  22876  m2cpmrngiso  22886  monmatcollpw  22907  pmatcollpwlem  22908  pmatcollpw  22909  pmatcollpwfi  22910  pmatcollpw3fi1lem2  22915  pmatcollpwscmat  22919  monmat2matmon  22952  pm2mp  22953  chpmatply1  22960  chpmat1d  22964  chpdmat  22969  chpscmat  22970  chpscmatgsumbin  22972  chpscmatgsummon  22973  chp0mat  22974  chpidmat  22975  chmaidscmat  22976  chfacfscmulcl  22985  chfacfscmul0  22986  chfacfscmulgsum  22988  chfacfpmmulcl  22989  chfacfpmmul0  22990  chfacfpmmulgsum  22992  chfacfpmmulgsum2  22993  cayhamlem1  22994  cpmadurid  22995  cpmidgsumm2pm  22997  cpmidpmatlem2  22999  cpmidpmatlem3  23000  cpmadugsumlemB  23002  cpmadugsumlemC  23003  cpmadugsumlemF  23004  cpmadugsumfi  23005  cpmidgsum2  23007  cpmadumatpolylem1  23009  cpmadumatpolylem2  23010  cpmadumatpoly  23011  cayhamlem2  23012  chcoeffeqlem  23013  cayhamlem4  23016  cayleyhamilton0  23017  cayleyhamiltonALT  23019  cayleyhamilton1  23020  fta1glem1  26296  fta1g  26298  fta1blem  26299  idomrootle  26301  dchrelbas3  27370  dchrelbasd  27371  dchrzrh1  27376  dchrzrhmul  27378  dchrmulcl  27381  dchrn0  27382  dchrfi  27387  dchrghm  27388  dchrabs  27392  dchrinv  27393  dchrptlem1  27396  dchrptlem2  27397  dchrptlem3  27398  dchrsum2  27400  dchrhash  27403  sum2dchr  27406  lgsqrlem1  27478  lgsqrlem2  27479  lgsqrlem3  27480  lgsqrlem4  27481  lgsdchr  27487  lgseisenlem3  27509  lgseisenlem4  27510  dchrisum0flblem1  27640  dchrisum0re  27645  unitprodclb  33648  ringlsmss1  33653  crngmxidl  33699  mxidlprm  33700  dflringlem3  33733  dflring3  33734  idlsrgmulrss1  33748  psrmonprod  33889  esplyfvaln  33911  mdetpmtr1  34160  mdetpmtr12  34162  madjusmdetlem1  34164  madjusmdetlem4  34167  mdetlap  34169  zarcls1  34206  zarclsint  34209  zarclssn  34210  zartopn  34212  zart0  34216  zarcmplem  34218  rspectps  34220  aks6d1c1p2  42803  aks6d1c1p7  42807  aks6d1c1p6  42808  aks6d1c1  42810  hashscontpowcl  42814  hashscontpow  42816  aks6d1c4  42818  aks6d1c2lem3  42820  aks6d1c2  42824  aks6d1c5lem1  42830  aks6d1c5lem3  42831  aks6d1c6lem1  42864  aks6d1c6lem3  42866  aks6d1c6lem5  42871  aks6d1c7lem1  42874  aks5lem1  42880  aks5lem2  42881  aks5lem5a  42885  frlmpwfi  43754  isnumbasgrplem3  43761  mendlmod  43845  idomodle  43847  2zrng0  48935  cznabel  48951  cznrng  48952  crhmsubcALTV  49018  fldcatALTV  49022  fldhmsubcALTV  49024  crngprmringidom  49032  mgpsumz  49064  mgpsumn  49065  evl1at0  49093  evl1at1  49094