Theorem crngring 20140

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6544  CMndccmn 19690  mulGrpcmgp 20029  Ringcrg 20128  CRingccrg 20129

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-cring 20131

This theorem is referenced by:  crngringd  20141  gsummgp0  20207  prdscrngd  20211  crngbinom  20224  dvdsunit  20271  unitmulclb  20273  unitabl  20276  rdivmuldivd  20305  idsrngd  20614  rmodislmod  20685  rmodislmodOLD  20686  quscrng  21030  cnring  21168  zringring  21221  zring0  21230  znzrh2  21321  zncyg  21324  zndvds0  21326  znf1o  21327  zzngim  21328  znfld  21336  znchr  21338  znunit  21339  znrrg  21341  cygznlem3  21345  re0g  21385  sraassa  21643  sraassaOLD  21644  rlmassa  21645  psrcrng  21753  mplcrng  21800  mplassa  21801  mplcoe2  21816  mplbas2  21817  mplmon2mul  21850  mplind  21851  evlslem2  21862  evlslem3  21863  evlslem6  21864  evlseu  21866  evlsval2  21870  evlsgsumadd  21874  evlsgsummul  21875  evlrhm  21879  evlsscasrng  21880  evlsca  21881  evlsvarsrng  21882  evlvar  21883  mpfind  21890  ply1crng  21942  ply1assa  21943  lply1binom  22051  lply1binomsc  22052  evls1rhmlem  22061  evls1gsumadd  22064  evls1gsummul  22065  evl1val  22069  evl1sca  22074  evl1scad  22075  evl1var  22076  evl1vard  22077  evls1var  22078  evls1scasrng  22079  evls1varsrng  22080  evl1subd  22082  evl1expd  22085  pf1const  22086  pf1id  22087  pf1ind  22095  evl1gsumdlem  22096  evl1gsumd  22097  evl1gsumadd  22098  evl1gsummul  22100  evl1varpw  22101  evl1scvarpw  22103  evl1scvarpwval  22104  evl1gsummon  22105  mamuvs2  22127  matassa  22167  madetsumid  22184  madetsmelbas  22187  madetsmelbas2  22188  mat1dimcrng  22200  dmatcrng  22225  scmatcrng  22244  mdetleib2  22311  mdetf  22318  m1detdiag  22320  mdetdiaglem  22321  mdetdiag  22322  mdet1  22324  mdetrlin  22325  mdetrsca2  22327  mdetr0  22328  mdet0  22329  mdetrlin2  22330  mdetralt  22331  mdetero  22333  mdetmul  22346  maducoeval2  22363  maduf  22364  madutpos  22365  madugsum  22366  madurid  22367  madulid  22368  marep01ma  22383  smadiadetlem0  22384  smadiadetlem1a  22386  smadiadetlem3lem2  22390  smadiadetlem3  22391  smadiadetlem4  22392  smadiadet  22393  smadiadetglem1  22394  smadiadetglem2  22395  smadiadetg  22396  matinv  22400  matunit  22401  slesolinv  22403  slesolinvbi  22404  slesolex  22405  cramerimplem1  22406  cramerimplem2  22407  cramerimplem3  22408  cramerimp  22409  cramer  22414  mat2pmatmul  22454  mat2pmatmhm  22456  mat2pmatrhm  22457  mat2pmatlin  22458  m2cpmmhm  22468  m2cpmrhm  22469  m2pmfzgsumcl  22471  m2cpmrngiso  22481  monmatcollpw  22502  pmatcollpwlem  22503  pmatcollpw  22504  pmatcollpwfi  22505  pmatcollpw3fi1lem2  22510  pmatcollpwscmat  22514  monmat2matmon  22547  pm2mp  22548  chpmatply1  22555  chpmat1d  22559  chpdmat  22564  chpscmat  22565  chpscmatgsumbin  22567  chpscmatgsummon  22568  chp0mat  22569  chpidmat  22570  chmaidscmat  22571  chfacfscmulcl  22580  chfacfscmul0  22581  chfacfscmulgsum  22583  chfacfpmmulcl  22584  chfacfpmmul0  22585  chfacfpmmulgsum  22587  chfacfpmmulgsum2  22588  cayhamlem1  22589  cpmadurid  22590  cpmidgsumm2pm  22592  cpmidpmatlem2  22594  cpmidpmatlem3  22595  cpmadugsumlemB  22597  cpmadugsumlemC  22598  cpmadugsumlemF  22599  cpmadugsumfi  22600  cpmidgsum2  22602  cpmadumatpolylem1  22604  cpmadumatpolylem2  22605  cpmadumatpoly  22606  cayhamlem2  22607  chcoeffeqlem  22608  cayhamlem4  22611  cayleyhamilton0  22612  cayleyhamiltonALT  22614  cayleyhamilton1  22615  recvsOLD  24895  fta1glem1  25916  fta1g  25918  fta1blem  25919  dchrelbas3  26974  dchrelbasd  26975  dchrzrh1  26980  dchrzrhmul  26982  dchrmulcl  26985  dchrn0  26986  dchrfi  26991  dchrghm  26992  dchrabs  26996  dchrinv  26997  dchrptlem1  27000  dchrptlem2  27001  dchrptlem3  27002  dchrsum2  27004  dchrhash  27007  sum2dchr  27010  lgsqrlem1  27082  lgsqrlem2  27083  lgsqrlem3  27084  lgsqrlem4  27085  lgsdchr  27091  lgseisenlem3  27113  lgseisenlem4  27114  dchrisum0flblem1  27244  dchrisum0re  27249  freshmansdream  32648  subofld  32701  ringlsmss1  32777  isprmidlc  32837  prmidl0  32840  qsidomlem1  32842  qsidomlem2  32843  crngmxidl  32856  mxidlprm  32857  idlsrgmulrss1  32896  evls1vsca  32921  ply1chr  32932  mdetpmtr1  33098  mdetpmtr12  33100  madjusmdetlem1  33102  madjusmdetlem4  33105  mdetlap  33107  zarcls1  33144  zarclsint  33147  zarclssn  33148  zartopn  33150  zart0  33154  zarcmplem  33156  rspectps  33158  selvcllem5  41457  frlmpwfi  42143  isnumbasgrplem3  42150  mendlmod  42238  idomrootle  42240  idomodle  42241  2zrng0  46926  cznabel  46942  cznrng  46943  crhmsubc  47066  fldcat  47070  fldhmsubc  47072  crhmsubcALTV  47084  fldcatALTV  47088  fldhmsubcALTV  47090  mgpsumz  47128  mgpsumn  47129  evl1at0  47161  evl1at1  47162