Theorem crngring 20217

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6492  CMndccmn 19746  mulGrpcmgp 20112  Ringcrg 20205  CRingccrg 20206

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-cring 20208

This theorem is referenced by:  crngringd  20218  gsummgp0  20288  prdscrngd  20292  crngbinom  20306  dvdsunit  20350  unitmulclb  20352  unitabl  20355  rdivmuldivd  20384  crhmsubc  20650  fldcat  20751  fldhmsubc  20753  idsrngd  20824  subofld  20845  rmodislmod  20916  quscrng  21273  cnring  21380  zringring  21439  zring0  21448  znzrh2  21535  zncyg  21538  zndvds0  21540  znf1o  21541  zzngim  21542  znfld  21550  znchr  21552  znunit  21553  znrrg  21555  cygznlem3  21559  freshmansdream  21564  re0g  21602  sraassa  21859  rlmassa  21860  psrcrng  21960  mplcrng  22009  mplassa  22010  mplcoe2  22029  mplbas2  22030  mplmon2mul  22057  mplind  22058  evlslem2  22067  evlslem3  22068  evlslem6  22069  evlseu  22071  evlsval2  22075  evlsgsumadd  22084  evlsgsummul  22085  evlrhm  22089  evlsscasrng  22093  evlsca  22094  evlsvarsrng  22095  evlvar  22096  mpfind  22103  ply1crng  22172  ply1assa  22173  ply1chr  22281  lply1binom  22285  lply1binomsc  22286  evls1rhmlem  22296  evls1gsumadd  22299  evls1gsummul  22300  evl1val  22304  evl1sca  22309  evl1scad  22310  evl1var  22311  evl1vard  22312  evls1var  22313  evls1scasrng  22314  evls1varsrng  22315  evl1subd  22317  evl1expd  22320  pf1const  22321  pf1id  22322  pf1ind  22330  evl1gsumdlem  22331  evl1gsumd  22332  evl1gsumadd  22333  evl1gsummul  22335  evl1varpw  22336  evl1scvarpw  22338  evl1scvarpwval  22339  evl1gsummon  22340  evls1vsca  22348  mamuvs2  22381  matassa  22419  madetsumid  22436  madetsmelbas  22439  madetsmelbas2  22440  mat1dimcrng  22452  dmatcrng  22477  scmatcrng  22496  mdetleib2  22563  mdetf  22570  m1detdiag  22572  mdetdiaglem  22573  mdetdiag  22574  mdet1  22576  mdetrlin  22577  mdetrsca2  22579  mdetr0  22580  mdet0  22581  mdetrlin2  22582  mdetralt  22583  mdetero  22585  mdetmul  22598  maducoeval2  22615  maduf  22616  madutpos  22617  madugsum  22618  madurid  22619  madulid  22620  marep01ma  22635  smadiadetlem0  22636  smadiadetlem1a  22638  smadiadetlem3lem2  22642  smadiadetlem3  22643  smadiadetlem4  22644  smadiadet  22645  smadiadetglem1  22646  smadiadetglem2  22647  smadiadetg  22648  matinv  22652  matunit  22653  slesolinv  22655  slesolinvbi  22656  slesolex  22657  cramerimplem1  22658  cramerimplem2  22659  cramerimplem3  22660  cramerimp  22661  cramer  22666  mat2pmatmul  22706  mat2pmatmhm  22708  mat2pmatrhm  22709  mat2pmatlin  22710  m2cpmmhm  22720  m2cpmrhm  22721  m2pmfzgsumcl  22723  m2cpmrngiso  22733  monmatcollpw  22754  pmatcollpwlem  22755  pmatcollpw  22756  pmatcollpwfi  22757  pmatcollpw3fi1lem2  22762  pmatcollpwscmat  22766  monmat2matmon  22799  pm2mp  22800  chpmatply1  22807  chpmat1d  22811  chpdmat  22816  chpscmat  22817  chpscmatgsumbin  22819  chpscmatgsummon  22820  chp0mat  22821  chpidmat  22822  chmaidscmat  22823  chfacfscmulcl  22832  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmulcl  22836  chfacfpmmul0  22837  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadurid  22842  cpmidgsumm2pm  22844  cpmidpmatlem2  22846  cpmidpmatlem3  22847  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cpmadugsumfi  22852  cpmidgsum2  22854  cpmadumatpolylem1  22856  cpmadumatpolylem2  22857  cpmadumatpoly  22858  cayhamlem2  22859  chcoeffeqlem  22860  cayhamlem4  22863  cayleyhamilton0  22864  cayleyhamiltonALT  22866  cayleyhamilton1  22867  fta1glem1  26143  fta1g  26145  fta1blem  26146  idomrootle  26148  dchrelbas3  27215  dchrelbasd  27216  dchrzrh1  27221  dchrzrhmul  27223  dchrmulcl  27226  dchrn0  27227  dchrfi  27232  dchrghm  27233  dchrabs  27237  dchrinv  27238  dchrptlem1  27241  dchrptlem2  27242  dchrptlem3  27243  dchrsum2  27245  dchrhash  27248  sum2dchr  27251  lgsqrlem1  27323  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  lgsdchr  27332  lgseisenlem3  27354  lgseisenlem4  27355  dchrisum0flblem1  27485  dchrisum0re  27490  unitprodclb  33464  ringlsmss1  33471  isprmidlc  33522  prmidl0  33525  qsidomlem1  33527  qsidomlem2  33528  crngmxidl  33544  mxidlprm  33545  idlsrgmulrss1  33586  psrmonprod  33711  esplyfvaln  33733  mdetpmtr1  33983  mdetpmtr12  33985  madjusmdetlem1  33987  madjusmdetlem4  33990  mdetlap  33992  zarcls1  34029  zarclsint  34032  zarclssn  34033  zartopn  34035  zart0  34039  zarcmplem  34041  rspectps  34043  aks6d1c1p2  42562  aks6d1c1p7  42566  aks6d1c1p6  42567  aks6d1c1  42569  hashscontpowcl  42573  hashscontpow  42575  aks6d1c4  42577  aks6d1c2lem3  42579  aks6d1c2  42583  aks6d1c5lem1  42589  aks6d1c5lem3  42590  aks6d1c6lem1  42623  aks6d1c6lem3  42625  aks6d1c6lem5  42630  aks6d1c7lem1  42633  aks5lem1  42639  aks5lem2  42640  aks5lem5a  42644  frlmpwfi  43544  isnumbasgrplem3  43551  mendlmod  43635  idomodle  43637  2zrng0  48732  cznabel  48748  cznrng  48749  crhmsubcALTV  48815  fldcatALTV  48819  fldhmsubcALTV  48821  mgpsumz  48850  mgpsumn  48851  evl1at0  48879  evl1at1  48880