Theorem crngring 20242

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6561  CMndccmn 19798  mulGrpcmgp 20137  Ringcrg 20230  CRingccrg 20231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-cring 20233

This theorem is referenced by:  crngringd  20243  gsummgp0  20315  prdscrngd  20319  crngbinom  20332  dvdsunit  20379  unitmulclb  20381  unitabl  20384  rdivmuldivd  20413  crhmsubc  20682  fldcat  20784  fldhmsubc  20786  idsrngd  20857  rmodislmod  20928  quscrng  21293  cnring  21403  zringring  21460  zring0  21469  znzrh2  21564  zncyg  21567  zndvds0  21569  znf1o  21570  zzngim  21571  znfld  21579  znchr  21581  znunit  21582  znrrg  21584  cygznlem3  21588  freshmansdream  21593  re0g  21630  sraassa  21889  sraassaOLD  21890  rlmassa  21891  psrcrng  21992  mplcrng  22041  mplassa  22042  mplcoe2  22059  mplbas2  22060  mplmon2mul  22093  mplind  22094  evlslem2  22103  evlslem3  22104  evlslem6  22105  evlseu  22107  evlsval2  22111  evlsgsumadd  22115  evlsgsummul  22116  evlrhm  22120  evlsscasrng  22121  evlsca  22122  evlsvarsrng  22123  evlvar  22124  mpfind  22131  ply1crng  22200  ply1assa  22201  ply1chr  22310  lply1binom  22314  lply1binomsc  22315  evls1rhmlem  22325  evls1gsumadd  22328  evls1gsummul  22329  evl1val  22333  evl1sca  22338  evl1scad  22339  evl1var  22340  evl1vard  22341  evls1var  22342  evls1scasrng  22343  evls1varsrng  22344  evl1subd  22346  evl1expd  22349  pf1const  22350  pf1id  22351  pf1ind  22359  evl1gsumdlem  22360  evl1gsumd  22361  evl1gsumadd  22362  evl1gsummul  22364  evl1varpw  22365  evl1scvarpw  22367  evl1scvarpwval  22368  evl1gsummon  22369  evls1vsca  22377  mamuvs2  22410  matassa  22450  madetsumid  22467  madetsmelbas  22470  madetsmelbas2  22471  mat1dimcrng  22483  dmatcrng  22508  scmatcrng  22527  mdetleib2  22594  mdetf  22601  m1detdiag  22603  mdetdiaglem  22604  mdetdiag  22605  mdet1  22607  mdetrlin  22608  mdetrsca2  22610  mdetr0  22611  mdet0  22612  mdetrlin2  22613  mdetralt  22614  mdetero  22616  mdetmul  22629  maducoeval2  22646  maduf  22647  madutpos  22648  madugsum  22649  madurid  22650  madulid  22651  marep01ma  22666  smadiadetlem0  22667  smadiadetlem1a  22669  smadiadetlem3lem2  22673  smadiadetlem3  22674  smadiadetlem4  22675  smadiadet  22676  smadiadetglem1  22677  smadiadetglem2  22678  smadiadetg  22679  matinv  22683  matunit  22684  slesolinv  22686  slesolinvbi  22687  slesolex  22688  cramerimplem1  22689  cramerimplem2  22690  cramerimplem3  22691  cramerimp  22692  cramer  22697  mat2pmatmul  22737  mat2pmatmhm  22739  mat2pmatrhm  22740  mat2pmatlin  22741  m2cpmmhm  22751  m2cpmrhm  22752  m2pmfzgsumcl  22754  m2cpmrngiso  22764  monmatcollpw  22785  pmatcollpwlem  22786  pmatcollpw  22787  pmatcollpwfi  22788  pmatcollpw3fi1lem2  22793  pmatcollpwscmat  22797  monmat2matmon  22830  pm2mp  22831  chpmatply1  22838  chpmat1d  22842  chpdmat  22847  chpscmat  22848  chpscmatgsumbin  22850  chpscmatgsummon  22851  chp0mat  22852  chpidmat  22853  chmaidscmat  22854  chfacfscmulcl  22863  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmulcl  22867  chfacfpmmul0  22868  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmadurid  22873  cpmidgsumm2pm  22875  cpmidpmatlem2  22877  cpmidpmatlem3  22878  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmidgsum2  22885  cpmadumatpolylem1  22887  cpmadumatpolylem2  22888  cpmadumatpoly  22889  cayhamlem2  22890  chcoeffeqlem  22891  cayhamlem4  22894  cayleyhamilton0  22895  cayleyhamiltonALT  22897  cayleyhamilton1  22898  recvsOLD  25180  fta1glem1  26207  fta1g  26209  fta1blem  26210  idomrootle  26212  dchrelbas3  27282  dchrelbasd  27283  dchrzrh1  27288  dchrzrhmul  27290  dchrmulcl  27293  dchrn0  27294  dchrfi  27299  dchrghm  27300  dchrabs  27304  dchrinv  27305  dchrptlem1  27308  dchrptlem2  27309  dchrptlem3  27310  dchrsum2  27312  dchrhash  27315  sum2dchr  27318  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  lgsdchr  27399  lgseisenlem3  27421  lgseisenlem4  27422  dchrisum0flblem1  27552  dchrisum0re  27557  subofld  33346  unitprodclb  33417  ringlsmss1  33424  isprmidlc  33475  prmidl0  33478  qsidomlem1  33480  qsidomlem2  33481  crngmxidl  33497  mxidlprm  33498  idlsrgmulrss1  33539  mdetpmtr1  33822  mdetpmtr12  33824  madjusmdetlem1  33826  madjusmdetlem4  33829  mdetlap  33831  zarcls1  33868  zarclsint  33871  zarclssn  33872  zartopn  33874  zart0  33878  zarcmplem  33880  rspectps  33882  aks6d1c1p2  42110  aks6d1c1p7  42114  aks6d1c1p6  42115  aks6d1c1  42117  hashscontpowcl  42121  hashscontpow  42123  aks6d1c4  42125  aks6d1c2lem3  42127  aks6d1c2  42131  aks6d1c5lem1  42137  aks6d1c5lem3  42138  aks6d1c6lem1  42171  aks6d1c6lem3  42173  aks6d1c6lem5  42178  aks6d1c7lem1  42181  aks5lem1  42187  aks5lem2  42188  aks5lem5a  42192  frlmpwfi  43110  isnumbasgrplem3  43117  mendlmod  43201  idomodle  43203  2zrng0  48160  cznabel  48176  cznrng  48177  crhmsubcALTV  48243  fldcatALTV  48247  fldhmsubcALTV  48249  mgpsumz  48278  mgpsumn  48279  evl1at0  48308  evl1at1  48309