Theorem crngring 20068

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6544  CMndccmn 19648  mulGrpcmgp 19987  Ringcrg 20056  CRingccrg 20057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  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 20059

This theorem is referenced by:  crngringd  20069  gsummgp0  20130  prdscrngd  20135  crngbinom  20148  dvdsunit  20193  unitmulclb  20195  unitabl  20198  rdivmuldivd  20227  idsrngd  20470  rmodislmod  20540  rmodislmodOLD  20541  quscrng  20878  cnring  20967  zringring  21020  zring0  21028  znzrh2  21101  zncyg  21104  zndvds0  21106  znf1o  21107  zzngim  21108  znfld  21116  znchr  21118  znunit  21119  znrrg  21121  cygznlem3  21125  re0g  21165  sraassa  21423  sraassaOLD  21424  rlmassa  21425  psrcrng  21533  mplcrng  21580  mplassa  21581  mplcoe2  21596  mplbas2  21597  mplmon2mul  21630  mplind  21631  evlslem2  21642  evlslem3  21643  evlslem6  21644  evlseu  21646  evlsval2  21650  evlsgsumadd  21654  evlsgsummul  21655  evlrhm  21659  evlsscasrng  21660  evlsca  21661  evlsvarsrng  21662  evlvar  21663  mpfind  21670  ply1crng  21722  ply1assa  21723  lply1binom  21830  lply1binomsc  21831  evls1rhmlem  21840  evls1gsumadd  21843  evls1gsummul  21844  evl1val  21848  evl1sca  21853  evl1scad  21854  evl1var  21855  evl1vard  21856  evls1var  21857  evls1scasrng  21858  evls1varsrng  21859  evl1subd  21861  evl1expd  21864  pf1const  21865  pf1id  21866  pf1ind  21874  evl1gsumdlem  21875  evl1gsumd  21876  evl1gsumadd  21877  evl1gsummul  21879  evl1varpw  21880  evl1scvarpw  21882  evl1scvarpwval  21883  evl1gsummon  21884  mamuvs2  21906  matassa  21946  madetsumid  21963  madetsmelbas  21966  madetsmelbas2  21967  mat1dimcrng  21979  dmatcrng  22004  scmatcrng  22023  mdetleib2  22090  mdetf  22097  m1detdiag  22099  mdetdiaglem  22100  mdetdiag  22101  mdet1  22103  mdetrlin  22104  mdetrsca2  22106  mdetr0  22107  mdet0  22108  mdetrlin2  22109  mdetralt  22110  mdetero  22112  mdetmul  22125  maducoeval2  22142  maduf  22143  madutpos  22144  madugsum  22145  madurid  22146  madulid  22147  marep01ma  22162  smadiadetlem0  22163  smadiadetlem1a  22165  smadiadetlem3lem2  22169  smadiadetlem3  22170  smadiadetlem4  22171  smadiadet  22172  smadiadetglem1  22173  smadiadetglem2  22174  smadiadetg  22175  matinv  22179  matunit  22180  slesolinv  22182  slesolinvbi  22183  slesolex  22184  cramerimplem1  22185  cramerimplem2  22186  cramerimplem3  22187  cramerimp  22188  cramer  22193  mat2pmatmul  22233  mat2pmatmhm  22235  mat2pmatrhm  22236  mat2pmatlin  22237  m2cpmmhm  22247  m2cpmrhm  22248  m2pmfzgsumcl  22250  m2cpmrngiso  22260  monmatcollpw  22281  pmatcollpwlem  22282  pmatcollpw  22283  pmatcollpwfi  22284  pmatcollpw3fi1lem2  22289  pmatcollpwscmat  22293  monmat2matmon  22326  pm2mp  22327  chpmatply1  22334  chpmat1d  22338  chpdmat  22343  chpscmat  22344  chpscmatgsumbin  22346  chpscmatgsummon  22347  chp0mat  22348  chpidmat  22349  chmaidscmat  22350  chfacfscmulcl  22359  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmulcl  22363  chfacfpmmul0  22364  chfacfpmmulgsum  22366  chfacfpmmulgsum2  22367  cayhamlem1  22368  cpmadurid  22369  cpmidgsumm2pm  22371  cpmidpmatlem2  22373  cpmidpmatlem3  22374  cpmadugsumlemB  22376  cpmadugsumlemC  22377  cpmadugsumlemF  22378  cpmadugsumfi  22379  cpmidgsum2  22381  cpmadumatpolylem1  22383  cpmadumatpolylem2  22384  cpmadumatpoly  22385  cayhamlem2  22386  chcoeffeqlem  22387  cayhamlem4  22390  cayleyhamilton0  22391  cayleyhamiltonALT  22393  cayleyhamilton1  22394  recvsOLD  24663  fta1glem1  25683  fta1g  25685  fta1blem  25686  dchrelbas3  26741  dchrelbasd  26742  dchrzrh1  26747  dchrzrhmul  26749  dchrmulcl  26752  dchrn0  26753  dchrfi  26758  dchrghm  26759  dchrabs  26763  dchrinv  26764  dchrptlem1  26767  dchrptlem2  26768  dchrptlem3  26769  dchrsum2  26771  dchrhash  26774  sum2dchr  26777  lgsqrlem1  26849  lgsqrlem2  26850  lgsqrlem3  26851  lgsqrlem4  26852  lgsdchr  26858  lgseisenlem3  26880  lgseisenlem4  26881  dchrisum0flblem1  27011  dchrisum0re  27016  freshmansdream  32381  subofld  32434  ringlsmss1  32506  isprmidlc  32566  prmidl0  32569  qsidomlem1  32571  qsidomlem2  32572  crngmxidl  32585  mxidlprm  32586  idlsrgmulrss1  32625  evls1vsca  32650  ply1chr  32661  mdetpmtr1  32803  mdetpmtr12  32805  madjusmdetlem1  32807  madjusmdetlem4  32810  mdetlap  32812  zarcls1  32849  zarclsint  32852  zarclssn  32853  zartopn  32855  zart0  32859  zarcmplem  32861  rspectps  32863  selvcllem5  41154  frlmpwfi  41840  isnumbasgrplem3  41847  mendlmod  41935  idomrootle  41937  idomodle  41938  2zrng0  46836  cznabel  46852  cznrng  46853  crhmsubc  46976  fldcat  46980  fldhmsubc  46982  crhmsubcALTV  46994  fldcatALTV  46998  fldhmsubcALTV  47000  mgpsumz  47038  mgpsumn  47039  evl1at0  47072  evl1at1  47073