Theorem crngring 20226

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  CMndccmn 19755  mulGrpcmgp 20121  Ringcrg 20214  CRingccrg 20215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-cring 20217

This theorem is referenced by:  crngringd  20227  gsummgp0  20297  prdscrngd  20301  crngbinom  20315  dvdsunit  20359  unitmulclb  20361  unitabl  20364  rdivmuldivd  20393  crhmsubc  20659  fldcat  20760  fldhmsubc  20762  idsrngd  20833  subofld  20854  rmodislmod  20925  quscrng  21281  cnring  21374  zringring  21429  zring0  21438  znzrh2  21525  zncyg  21528  zndvds0  21530  znf1o  21531  zzngim  21532  znfld  21540  znchr  21542  znunit  21543  znrrg  21545  cygznlem3  21549  freshmansdream  21554  re0g  21592  sraassa  21849  rlmassa  21850  psrcrng  21950  mplcrng  21999  mplassa  22000  mplcoe2  22019  mplbas2  22020  mplmon2mul  22047  mplind  22048  evlslem2  22057  evlslem3  22058  evlslem6  22059  evlseu  22061  evlsval2  22065  evlsgsumadd  22074  evlsgsummul  22075  evlrhm  22079  evlsscasrng  22083  evlsca  22084  evlsvarsrng  22085  evlvar  22086  mpfind  22093  ply1crng  22162  ply1assa  22163  ply1chr  22271  lply1binom  22275  lply1binomsc  22276  evls1rhmlem  22286  evls1gsumadd  22289  evls1gsummul  22290  evl1val  22294  evl1sca  22299  evl1scad  22300  evl1var  22301  evl1vard  22302  evls1var  22303  evls1scasrng  22304  evls1varsrng  22305  evl1subd  22307  evl1expd  22310  pf1const  22311  pf1id  22312  pf1ind  22320  evl1gsumdlem  22321  evl1gsumd  22322  evl1gsumadd  22323  evl1gsummul  22325  evl1varpw  22326  evl1scvarpw  22328  evl1scvarpwval  22329  evl1gsummon  22330  evls1vsca  22338  mamuvs2  22371  matassa  22409  madetsumid  22426  madetsmelbas  22429  madetsmelbas2  22430  mat1dimcrng  22442  dmatcrng  22467  scmatcrng  22486  mdetleib2  22553  mdetf  22560  m1detdiag  22562  mdetdiaglem  22563  mdetdiag  22564  mdet1  22566  mdetrlin  22567  mdetrsca2  22569  mdetr0  22570  mdet0  22571  mdetrlin2  22572  mdetralt  22573  mdetero  22575  mdetmul  22588  maducoeval2  22605  maduf  22606  madutpos  22607  madugsum  22608  madurid  22609  madulid  22610  marep01ma  22625  smadiadetlem0  22626  smadiadetlem1a  22628  smadiadetlem3lem2  22632  smadiadetlem3  22633  smadiadetlem4  22634  smadiadet  22635  smadiadetglem1  22636  smadiadetglem2  22637  smadiadetg  22638  matinv  22642  matunit  22643  slesolinv  22645  slesolinvbi  22646  slesolex  22647  cramerimplem1  22648  cramerimplem2  22649  cramerimplem3  22650  cramerimp  22651  cramer  22656  mat2pmatmul  22696  mat2pmatmhm  22698  mat2pmatrhm  22699  mat2pmatlin  22700  m2cpmmhm  22710  m2cpmrhm  22711  m2pmfzgsumcl  22713  m2cpmrngiso  22723  monmatcollpw  22744  pmatcollpwlem  22745  pmatcollpw  22746  pmatcollpwfi  22747  pmatcollpw3fi1lem2  22752  pmatcollpwscmat  22756  monmat2matmon  22789  pm2mp  22790  chpmatply1  22797  chpmat1d  22801  chpdmat  22806  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  chp0mat  22811  chpidmat  22812  chmaidscmat  22813  chfacfscmulcl  22822  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmulcl  22826  chfacfpmmul0  22827  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadurid  22832  cpmidgsumm2pm  22834  cpmidpmatlem2  22836  cpmidpmatlem3  22837  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cpmadugsumfi  22842  cpmidgsum2  22844  cpmadumatpolylem1  22846  cpmadumatpolylem2  22847  cpmadumatpoly  22848  cayhamlem2  22849  chcoeffeqlem  22850  cayhamlem4  22853  cayleyhamilton0  22854  cayleyhamiltonALT  22856  cayleyhamilton1  22857  fta1glem1  26133  fta1g  26135  fta1blem  26136  idomrootle  26138  dchrelbas3  27201  dchrelbasd  27202  dchrzrh1  27207  dchrzrhmul  27209  dchrmulcl  27212  dchrn0  27213  dchrfi  27218  dchrghm  27219  dchrabs  27223  dchrinv  27224  dchrptlem1  27227  dchrptlem2  27228  dchrptlem3  27229  dchrsum2  27231  dchrhash  27234  sum2dchr  27237  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  lgsdchr  27318  lgseisenlem3  27340  lgseisenlem4  27341  dchrisum0flblem1  27471  dchrisum0re  27476  unitprodclb  33449  ringlsmss1  33456  isprmidlc  33507  prmidl0  33510  qsidomlem1  33512  qsidomlem2  33513  crngmxidl  33529  mxidlprm  33530  idlsrgmulrss1  33571  psrmonprod  33696  esplyfvaln  33718  mdetpmtr1  33967  mdetpmtr12  33969  madjusmdetlem1  33971  madjusmdetlem4  33974  mdetlap  33976  zarcls1  34013  zarclsint  34016  zarclssn  34017  zartopn  34019  zart0  34023  zarcmplem  34025  rspectps  34027  aks6d1c1p2  42548  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1  42555  hashscontpowcl  42559  hashscontpow  42561  aks6d1c4  42563  aks6d1c2lem3  42565  aks6d1c2  42569  aks6d1c5lem1  42575  aks6d1c5lem3  42576  aks6d1c6lem1  42609  aks6d1c6lem3  42611  aks6d1c6lem5  42616  aks6d1c7lem1  42619  aks5lem1  42625  aks5lem2  42626  aks5lem5a  42630  frlmpwfi  43526  isnumbasgrplem3  43533  mendlmod  43617  idomodle  43619  2zrng0  48720  cznabel  48736  cznrng  48737  crhmsubcALTV  48803  fldcatALTV  48807  fldhmsubcALTV  48809  mgpsumz  48838  mgpsumn  48839  evl1at0  48867  evl1at1  48868