Theorem crngring 20192

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6500  CMndccmn 19721  mulGrpcmgp 20087  Ringcrg 20180  CRingccrg 20181

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-cring 20183

This theorem is referenced by:  crngringd  20193  gsummgp0  20265  prdscrngd  20269  crngbinom  20283  dvdsunit  20327  unitmulclb  20329  unitabl  20332  rdivmuldivd  20361  crhmsubc  20627  fldcat  20728  fldhmsubc  20730  idsrngd  20801  subofld  20822  rmodislmod  20893  quscrng  21250  cnring  21357  zringring  21416  zring0  21425  znzrh2  21512  zncyg  21515  zndvds0  21517  znf1o  21518  zzngim  21519  znfld  21527  znchr  21529  znunit  21530  znrrg  21532  cygznlem3  21536  freshmansdream  21541  re0g  21579  sraassa  21836  sraassaOLD  21837  rlmassa  21838  psrcrng  21939  mplcrng  21988  mplassa  21989  mplcoe2  22008  mplbas2  22009  mplmon2mul  22036  mplind  22037  evlslem2  22046  evlslem3  22047  evlslem6  22048  evlseu  22050  evlsval2  22054  evlsgsumadd  22063  evlsgsummul  22064  evlrhm  22068  evlsscasrng  22072  evlsca  22073  evlsvarsrng  22074  evlvar  22075  mpfind  22082  ply1crng  22151  ply1assa  22152  ply1chr  22262  lply1binom  22266  lply1binomsc  22267  evls1rhmlem  22277  evls1gsumadd  22280  evls1gsummul  22281  evl1val  22285  evl1sca  22290  evl1scad  22291  evl1var  22292  evl1vard  22293  evls1var  22294  evls1scasrng  22295  evls1varsrng  22296  evl1subd  22298  evl1expd  22301  pf1const  22302  pf1id  22303  pf1ind  22311  evl1gsumdlem  22312  evl1gsumd  22313  evl1gsumadd  22314  evl1gsummul  22316  evl1varpw  22317  evl1scvarpw  22319  evl1scvarpwval  22320  evl1gsummon  22321  evls1vsca  22329  mamuvs2  22362  matassa  22400  madetsumid  22417  madetsmelbas  22420  madetsmelbas2  22421  mat1dimcrng  22433  dmatcrng  22458  scmatcrng  22477  mdetleib2  22544  mdetf  22551  m1detdiag  22553  mdetdiaglem  22554  mdetdiag  22555  mdet1  22557  mdetrlin  22558  mdetrsca2  22560  mdetr0  22561  mdet0  22562  mdetrlin2  22563  mdetralt  22564  mdetero  22566  mdetmul  22579  maducoeval2  22596  maduf  22597  madutpos  22598  madugsum  22599  madurid  22600  madulid  22601  marep01ma  22616  smadiadetlem0  22617  smadiadetlem1a  22619  smadiadetlem3lem2  22623  smadiadetlem3  22624  smadiadetlem4  22625  smadiadet  22626  smadiadetglem1  22627  smadiadetglem2  22628  smadiadetg  22629  matinv  22633  matunit  22634  slesolinv  22636  slesolinvbi  22637  slesolex  22638  cramerimplem1  22639  cramerimplem2  22640  cramerimplem3  22641  cramerimp  22642  cramer  22647  mat2pmatmul  22687  mat2pmatmhm  22689  mat2pmatrhm  22690  mat2pmatlin  22691  m2cpmmhm  22701  m2cpmrhm  22702  m2pmfzgsumcl  22704  m2cpmrngiso  22714  monmatcollpw  22735  pmatcollpwlem  22736  pmatcollpw  22737  pmatcollpwfi  22738  pmatcollpw3fi1lem2  22743  pmatcollpwscmat  22747  monmat2matmon  22780  pm2mp  22781  chpmatply1  22788  chpmat1d  22792  chpdmat  22797  chpscmat  22798  chpscmatgsumbin  22800  chpscmatgsummon  22801  chp0mat  22802  chpidmat  22803  chmaidscmat  22804  chfacfscmulcl  22813  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmulcl  22817  chfacfpmmul0  22818  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmadurid  22823  cpmidgsumm2pm  22825  cpmidpmatlem2  22827  cpmidpmatlem3  22828  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cpmadugsumfi  22833  cpmidgsum2  22835  cpmadumatpolylem1  22837  cpmadumatpolylem2  22838  cpmadumatpoly  22839  cayhamlem2  22840  chcoeffeqlem  22841  cayhamlem4  22844  cayleyhamilton0  22845  cayleyhamiltonALT  22847  cayleyhamilton1  22848  fta1glem1  26141  fta1g  26143  fta1blem  26144  idomrootle  26146  dchrelbas3  27217  dchrelbasd  27218  dchrzrh1  27223  dchrzrhmul  27225  dchrmulcl  27228  dchrn0  27229  dchrfi  27234  dchrghm  27235  dchrabs  27239  dchrinv  27240  dchrptlem1  27243  dchrptlem2  27244  dchrptlem3  27245  dchrsum2  27247  dchrhash  27250  sum2dchr  27253  lgsqrlem1  27325  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  lgsdchr  27334  lgseisenlem3  27356  lgseisenlem4  27357  dchrisum0flblem1  27487  dchrisum0re  27492  unitprodclb  33481  ringlsmss1  33488  isprmidlc  33539  prmidl0  33542  qsidomlem1  33544  qsidomlem2  33545  crngmxidl  33561  mxidlprm  33562  idlsrgmulrss1  33603  psrmonprod  33728  esplyfvaln  33750  mdetpmtr1  34000  mdetpmtr12  34002  madjusmdetlem1  34004  madjusmdetlem4  34007  mdetlap  34009  zarcls1  34046  zarclsint  34049  zarclssn  34050  zartopn  34052  zart0  34056  zarcmplem  34058  rspectps  34060  aks6d1c1p2  42476  aks6d1c1p7  42480  aks6d1c1p6  42481  aks6d1c1  42483  hashscontpowcl  42487  hashscontpow  42489  aks6d1c4  42491  aks6d1c2lem3  42493  aks6d1c2  42497  aks6d1c5lem1  42503  aks6d1c5lem3  42504  aks6d1c6lem1  42537  aks6d1c6lem3  42539  aks6d1c6lem5  42544  aks6d1c7lem1  42547  aks5lem1  42553  aks5lem2  42554  aks5lem5a  42558  frlmpwfi  43452  isnumbasgrplem3  43459  mendlmod  43543  idomodle  43545  2zrng0  48601  cznabel  48617  cznrng  48618  crhmsubcALTV  48684  fldcatALTV  48688  fldhmsubcALTV  48690  mgpsumz  48719  mgpsumn  48720  evl1at0  48748  evl1at1  48749