Theorem crngring 20224

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

Syntax hints:   → wi 4   ∈ wcel 2119  ‘cfv 6492  CMndccmn 19753  mulGrpcmgp 20119  Ringcrg 20212  CRingccrg 20213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-cring 20215

This theorem is referenced by:  crngringd  20225  gsummgp0  20295  prdscrngd  20299  crngbinom  20313  dvdsunit  20357  unitmulclb  20359  unitabl  20362  rdivmuldivd  20391  crhmsubc  20661  fldcat  20762  fldhmsubc  20764  idsrngd  20835  subofld  20856  rmodislmod  20927  quscrng  21283  cnring  21376  zringring  21431  zring0  21440  znzrh2  21527  zncyg  21530  zndvds0  21532  znf1o  21533  zzngim  21534  znfld  21542  znchr  21544  znunit  21545  znrrg  21547  cygznlem3  21551  freshmansdream  21556  re0g  21594  sraassa  21851  rlmassa  21852  psrcrng  21953  mplcrng  22002  mplassa  22003  mplcoe2  22024  mplbas2  22025  mplmon2mul  22052  mplind  22053  evlslem2  22062  evlslem3  22063  evlslem6  22064  evlseu  22066  evlsval2  22070  evlsgsumadd  22079  evlsgsummul  22080  evlrhm  22084  evlsscasrng  22088  evlsca  22089  evlsvarsrng  22090  evlvar  22091  mpfind  22098  ply1crng  22190  ply1assa  22191  ply1chr  22299  lply1binom  22303  lply1binomsc  22304  evls1rhmlem  22314  evls1gsumadd  22317  evls1gsummul  22318  evl1val  22322  evl1sca  22327  evl1scad  22328  evl1var  22329  evl1vard  22330  evls1var  22331  evls1scasrng  22332  evls1varsrng  22333  evl1subd  22335  evl1expd  22338  pf1const  22339  pf1id  22340  pf1ind  22348  evl1gsumdlem  22349  evl1gsumd  22350  evl1gsumadd  22351  evl1gsummul  22353  evl1varpw  22354  evl1scvarpw  22356  evl1scvarpwval  22357  evl1gsummon  22358  evls1vsca  22366  mamuvs2  22396  matassa  22434  madetsumid  22451  madetsmelbas  22454  madetsmelbas2  22455  mat1dimcrng  22467  dmatcrng  22492  scmatcrng  22511  mdetleib2  22578  mdetf  22585  m1detdiag  22587  mdetdiaglem  22588  mdetdiag  22589  mdet1  22591  mdetrlin  22592  mdetrsca2  22594  mdetr0  22595  mdet0  22596  mdetrlin2  22597  mdetralt  22598  mdetero  22600  mdetmul  22613  maducoeval2  22630  maduf  22631  madutpos  22632  madugsum  22633  madurid  22634  madulid  22635  marep01ma  22650  smadiadetlem0  22651  smadiadetlem1a  22653  smadiadetlem3lem2  22657  smadiadetlem3  22658  smadiadetlem4  22659  smadiadet  22660  smadiadetglem1  22661  smadiadetglem2  22662  smadiadetg  22663  matinv  22667  matunit  22668  slesolinv  22670  slesolinvbi  22671  slesolex  22672  cramerimplem1  22673  cramerimplem2  22674  cramerimplem3  22675  cramerimp  22676  cramer  22681  mat2pmatmul  22721  mat2pmatmhm  22723  mat2pmatrhm  22724  mat2pmatlin  22725  m2cpmmhm  22735  m2cpmrhm  22736  m2pmfzgsumcl  22738  m2cpmrngiso  22748  monmatcollpw  22769  pmatcollpwlem  22770  pmatcollpw  22771  pmatcollpwfi  22772  pmatcollpw3fi1lem2  22777  pmatcollpwscmat  22781  monmat2matmon  22814  pm2mp  22815  chpmatply1  22822  chpmat1d  22826  chpdmat  22831  chpscmat  22832  chpscmatgsumbin  22834  chpscmatgsummon  22835  chp0mat  22836  chpidmat  22837  chmaidscmat  22838  chfacfscmulcl  22847  chfacfscmul0  22848  chfacfscmulgsum  22850  chfacfpmmulcl  22851  chfacfpmmul0  22852  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmadurid  22857  cpmidgsumm2pm  22859  cpmidpmatlem2  22861  cpmidpmatlem3  22862  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cpmadugsumfi  22867  cpmidgsum2  22869  cpmadumatpolylem1  22871  cpmadumatpolylem2  22872  cpmadumatpoly  22873  cayhamlem2  22874  chcoeffeqlem  22875  cayhamlem4  22878  cayleyhamilton0  22879  cayleyhamiltonALT  22881  cayleyhamilton1  22882  fta1glem1  26158  fta1g  26160  fta1blem  26161  idomrootle  26163  dchrelbas3  27226  dchrelbasd  27227  dchrzrh1  27232  dchrzrhmul  27234  dchrmulcl  27237  dchrn0  27238  dchrfi  27243  dchrghm  27244  dchrabs  27248  dchrinv  27249  dchrptlem1  27252  dchrptlem2  27253  dchrptlem3  27254  dchrsum2  27256  dchrhash  27259  sum2dchr  27262  lgsqrlem1  27334  lgsqrlem2  27335  lgsqrlem3  27336  lgsqrlem4  27337  lgsdchr  27343  lgseisenlem3  27365  lgseisenlem4  27366  dchrisum0flblem1  27496  dchrisum0re  27501  unitprodclb  33479  ringlsmss1  33486  isprmidlc  33537  prmidl0  33540  qsidomlem1  33542  qsidomlem2  33543  crngmxidl  33559  mxidlprm  33560  idlsrgmulrss1  33601  psrmonprod  33743  esplyfvaln  33765  mdetpmtr1  34014  mdetpmtr12  34016  madjusmdetlem1  34018  madjusmdetlem4  34021  mdetlap  34023  zarcls1  34060  zarclsint  34063  zarclssn  34064  zartopn  34066  zart0  34070  zarcmplem  34072  rspectps  34074  aks6d1c1p2  42601  aks6d1c1p7  42605  aks6d1c1p6  42606  aks6d1c1  42608  hashscontpowcl  42612  hashscontpow  42614  aks6d1c4  42616  aks6d1c2lem3  42618  aks6d1c2  42622  aks6d1c5lem1  42628  aks6d1c5lem3  42629  aks6d1c6lem1  42662  aks6d1c6lem3  42664  aks6d1c6lem5  42669  aks6d1c7lem1  42672  aks5lem1  42678  aks5lem2  42679  aks5lem5a  42683  frlmpwfi  43550  isnumbasgrplem3  43557  mendlmod  43641  idomodle  43643  2zrng0  48742  cznabel  48758  cznrng  48759  crhmsubcALTV  48825  fldcatALTV  48829  fldhmsubcALTV  48831  mgpsumz  48860  mgpsumn  48861  evl1at0  48889  evl1at1  48890