Theorem crngring 20262

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  CMndccmn 19812  mulGrpcmgp 20151  Ringcrg 20250  CRingccrg 20251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-cring 20253

This theorem is referenced by:  crngringd  20263  gsummgp0  20331  prdscrngd  20335  crngbinom  20348  dvdsunit  20395  unitmulclb  20397  unitabl  20400  rdivmuldivd  20429  crhmsubc  20698  fldcat  20800  fldhmsubc  20802  idsrngd  20873  rmodislmod  20944  rmodislmodOLD  20945  quscrng  21310  cnring  21420  zringring  21477  zring0  21486  znzrh2  21581  zncyg  21584  zndvds0  21586  znf1o  21587  zzngim  21588  znfld  21596  znchr  21598  znunit  21599  znrrg  21601  cygznlem3  21605  freshmansdream  21610  re0g  21647  sraassa  21906  sraassaOLD  21907  rlmassa  21908  psrcrng  22009  mplcrng  22058  mplassa  22059  mplcoe2  22076  mplbas2  22077  mplmon2mul  22110  mplind  22111  evlslem2  22120  evlslem3  22121  evlslem6  22122  evlseu  22124  evlsval2  22128  evlsgsumadd  22132  evlsgsummul  22133  evlrhm  22137  evlsscasrng  22138  evlsca  22139  evlsvarsrng  22140  evlvar  22141  mpfind  22148  ply1crng  22215  ply1assa  22216  ply1chr  22325  lply1binom  22329  lply1binomsc  22330  evls1rhmlem  22340  evls1gsumadd  22343  evls1gsummul  22344  evl1val  22348  evl1sca  22353  evl1scad  22354  evl1var  22355  evl1vard  22356  evls1var  22357  evls1scasrng  22358  evls1varsrng  22359  evl1subd  22361  evl1expd  22364  pf1const  22365  pf1id  22366  pf1ind  22374  evl1gsumdlem  22375  evl1gsumd  22376  evl1gsumadd  22377  evl1gsummul  22379  evl1varpw  22380  evl1scvarpw  22382  evl1scvarpwval  22383  evl1gsummon  22384  evls1vsca  22392  mamuvs2  22425  matassa  22465  madetsumid  22482  madetsmelbas  22485  madetsmelbas2  22486  mat1dimcrng  22498  dmatcrng  22523  scmatcrng  22542  mdetleib2  22609  mdetf  22616  m1detdiag  22618  mdetdiaglem  22619  mdetdiag  22620  mdet1  22622  mdetrlin  22623  mdetrsca2  22625  mdetr0  22626  mdet0  22627  mdetrlin2  22628  mdetralt  22629  mdetero  22631  mdetmul  22644  maducoeval2  22661  maduf  22662  madutpos  22663  madugsum  22664  madurid  22665  madulid  22666  marep01ma  22681  smadiadetlem0  22682  smadiadetlem1a  22684  smadiadetlem3lem2  22688  smadiadetlem3  22689  smadiadetlem4  22690  smadiadet  22691  smadiadetglem1  22692  smadiadetglem2  22693  smadiadetg  22694  matinv  22698  matunit  22699  slesolinv  22701  slesolinvbi  22702  slesolex  22703  cramerimplem1  22704  cramerimplem2  22705  cramerimplem3  22706  cramerimp  22707  cramer  22712  mat2pmatmul  22752  mat2pmatmhm  22754  mat2pmatrhm  22755  mat2pmatlin  22756  m2cpmmhm  22766  m2cpmrhm  22767  m2pmfzgsumcl  22769  m2cpmrngiso  22779  monmatcollpw  22800  pmatcollpwlem  22801  pmatcollpw  22802  pmatcollpwfi  22803  pmatcollpw3fi1lem2  22808  pmatcollpwscmat  22812  monmat2matmon  22845  pm2mp  22846  chpmatply1  22853  chpmat1d  22857  chpdmat  22862  chpscmat  22863  chpscmatgsumbin  22865  chpscmatgsummon  22866  chp0mat  22867  chpidmat  22868  chmaidscmat  22869  chfacfscmulcl  22878  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmulcl  22882  chfacfpmmul0  22883  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadurid  22888  cpmidgsumm2pm  22890  cpmidpmatlem2  22892  cpmidpmatlem3  22893  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cpmadugsumfi  22898  cpmidgsum2  22900  cpmadumatpolylem1  22902  cpmadumatpolylem2  22903  cpmadumatpoly  22904  cayhamlem2  22905  chcoeffeqlem  22906  cayhamlem4  22909  cayleyhamilton0  22910  cayleyhamiltonALT  22912  cayleyhamilton1  22913  recvsOLD  25193  fta1glem1  26221  fta1g  26223  fta1blem  26224  idomrootle  26226  dchrelbas3  27296  dchrelbasd  27297  dchrzrh1  27302  dchrzrhmul  27304  dchrmulcl  27307  dchrn0  27308  dchrfi  27313  dchrghm  27314  dchrabs  27318  dchrinv  27319  dchrptlem1  27322  dchrptlem2  27323  dchrptlem3  27324  dchrsum2  27326  dchrhash  27329  sum2dchr  27332  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  lgsdchr  27413  lgseisenlem3  27435  lgseisenlem4  27436  dchrisum0flblem1  27566  dchrisum0re  27571  subofld  33325  unitprodclb  33396  ringlsmss1  33403  isprmidlc  33454  prmidl0  33457  qsidomlem1  33459  qsidomlem2  33460  crngmxidl  33476  mxidlprm  33477  idlsrgmulrss1  33518  mdetpmtr1  33783  mdetpmtr12  33785  madjusmdetlem1  33787  madjusmdetlem4  33790  mdetlap  33792  zarcls1  33829  zarclsint  33832  zarclssn  33833  zartopn  33835  zart0  33839  zarcmplem  33841  rspectps  33843  aks6d1c1p2  42090  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1  42097  hashscontpowcl  42101  hashscontpow  42103  aks6d1c4  42105  aks6d1c2lem3  42107  aks6d1c2  42111  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c6lem1  42151  aks6d1c6lem3  42153  aks6d1c6lem5  42158  aks6d1c7lem1  42161  aks5lem1  42167  aks5lem2  42168  aks5lem5a  42172  frlmpwfi  43086  isnumbasgrplem3  43093  mendlmod  43177  idomodle  43179  2zrng0  48087  cznabel  48103  cznrng  48104  crhmsubcALTV  48170  fldcatALTV  48174  fldhmsubcALTV  48176  mgpsumz  48206  mgpsumn  48207  evl1at0  48236  evl1at1  48237