Theorem crngring 20281

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

Syntax hints:   → wi 4   ∈ wcel 2141  ‘cfv 6515  CMndccmn 19810  mulGrpcmgp 20176  Ringcrg 20269  CRingccrg 20270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6471  df-fv 6523  df-cring 20272

This theorem is referenced by:  crngringd  20282  gsummgp0  20352  prdscrngd  20356  crngbinom  20370  dvdsunit  20414  unitmulclb  20416  unitabl  20419  rdivmuldivd  20448  crhmsubc  20718  fldcat  20819  fldhmsubc  20821  idsrngd  20892  subofld  20913  rmodislmod  20984  quscrng  21340  cnring  21433  zringring  21488  zring0  21497  znzrh2  21584  zncyg  21587  zndvds0  21589  znf1o  21590  zzngim  21591  znfld  21599  znchr  21601  znunit  21602  znrrg  21604  cygznlem3  21608  freshmansdream  21613  re0g  21651  sraassa  21908  rlmassa  21909  psrcrng  22010  mplcrng  22059  mplassa  22060  mplcoe2  22081  mplbas2  22082  mplmon2mul  22109  mplind  22110  evlslem2  22119  evlslem3  22120  evlslem6  22121  evlseu  22123  evlsval2  22127  evlsgsumadd  22136  evlsgsummul  22137  evlrhm  22141  evlsscasrng  22145  evlsca  22146  evlsvarsrng  22147  evlvar  22148  mpfind  22155  ply1crng  22247  ply1assa  22248  ply1chr  22356  lply1binom  22360  lply1binomsc  22361  evls1rhmlem  22371  evls1gsumadd  22374  evls1gsummul  22375  evl1val  22379  evl1sca  22384  evl1scad  22385  evl1var  22386  evl1vard  22387  evls1var  22388  evls1scasrng  22389  evls1varsrng  22390  evl1subd  22392  evl1expd  22395  pf1const  22396  pf1id  22397  pf1ind  22405  evl1gsumdlem  22406  evl1gsumd  22407  evl1gsumadd  22408  evl1gsummul  22410  evl1varpw  22411  evl1scvarpw  22413  evl1scvarpwval  22414  evl1gsummon  22415  evls1vsca  22423  mamuvs2  22453  matassa  22491  madetsumid  22508  madetsmelbas  22511  madetsmelbas2  22512  mat1dimcrng  22524  dmatcrng  22549  scmatcrng  22568  mdetleib2  22635  mdetf  22642  m1detdiag  22644  mdetdiaglem  22645  mdetdiag  22646  mdet1  22648  mdetrlin  22649  mdetrsca2  22651  mdetr0  22652  mdet0  22653  mdetrlin2  22654  mdetralt  22655  mdetero  22657  mdetmul  22670  maducoeval2  22687  maduf  22688  madutpos  22689  madugsum  22690  madurid  22691  madulid  22692  marep01ma  22707  smadiadetlem0  22708  smadiadetlem1a  22710  smadiadetlem3lem2  22714  smadiadetlem3  22715  smadiadetlem4  22716  smadiadet  22717  smadiadetglem1  22718  smadiadetglem2  22719  smadiadetg  22720  matinv  22724  matunit  22725  slesolinv  22727  slesolinvbi  22728  slesolex  22729  cramerimplem1  22730  cramerimplem2  22731  cramerimplem3  22732  cramerimp  22733  cramer  22738  mat2pmatmul  22778  mat2pmatmhm  22780  mat2pmatrhm  22781  mat2pmatlin  22782  m2cpmmhm  22792  m2cpmrhm  22793  m2pmfzgsumcl  22795  m2cpmrngiso  22805  monmatcollpw  22826  pmatcollpwlem  22827  pmatcollpw  22828  pmatcollpwfi  22829  pmatcollpw3fi1lem2  22834  pmatcollpwscmat  22838  monmat2matmon  22871  pm2mp  22872  chpmatply1  22879  chpmat1d  22883  chpdmat  22888  chpscmat  22889  chpscmatgsumbin  22891  chpscmatgsummon  22892  chp0mat  22893  chpidmat  22894  chmaidscmat  22895  chfacfscmulcl  22904  chfacfscmul0  22905  chfacfscmulgsum  22907  chfacfpmmulcl  22908  chfacfpmmul0  22909  chfacfpmmulgsum  22911  chfacfpmmulgsum2  22912  cayhamlem1  22913  cpmadurid  22914  cpmidgsumm2pm  22916  cpmidpmatlem2  22918  cpmidpmatlem3  22919  cpmadugsumlemB  22921  cpmadugsumlemC  22922  cpmadugsumlemF  22923  cpmadugsumfi  22924  cpmidgsum2  22926  cpmadumatpolylem1  22928  cpmadumatpolylem2  22929  cpmadumatpoly  22930  cayhamlem2  22931  chcoeffeqlem  22932  cayhamlem4  22935  cayleyhamilton0  22936  cayleyhamiltonALT  22938  cayleyhamilton1  22939  fta1glem1  26215  fta1g  26217  fta1blem  26218  idomrootle  26220  dchrelbas3  27289  dchrelbasd  27290  dchrzrh1  27295  dchrzrhmul  27297  dchrmulcl  27300  dchrn0  27301  dchrfi  27306  dchrghm  27307  dchrabs  27311  dchrinv  27312  dchrptlem1  27315  dchrptlem2  27316  dchrptlem3  27317  dchrsum2  27319  dchrhash  27322  sum2dchr  27325  lgsqrlem1  27397  lgsqrlem2  27398  lgsqrlem3  27399  lgsqrlem4  27400  lgsdchr  27406  lgseisenlem3  27428  lgseisenlem4  27429  dchrisum0flblem1  27559  dchrisum0re  27564  unitprodclb  33535  ringlsmss1  33542  isprmidlc  33593  prmidl0  33597  qsidomlem1  33599  qsidomlem2  33600  prmidlsubm  33606  crngmxidl  33617  mxidlprm  33618  dflringlem3  33652  dflring3  33653  idlsrgmulrss1  33667  psrmonprod  33809  esplyfvaln  33831  mdetpmtr1  34080  mdetpmtr12  34082  madjusmdetlem1  34084  madjusmdetlem4  34087  mdetlap  34089  zarcls1  34126  zarclsint  34129  zarclssn  34130  zartopn  34132  zart0  34136  zarcmplem  34138  rspectps  34140  aks6d1c1p2  42686  aks6d1c1p7  42690  aks6d1c1p6  42691  aks6d1c1  42693  hashscontpowcl  42697  hashscontpow  42699  aks6d1c4  42701  aks6d1c2lem3  42703  aks6d1c2  42707  aks6d1c5lem1  42713  aks6d1c5lem3  42714  aks6d1c6lem1  42747  aks6d1c6lem3  42749  aks6d1c6lem5  42754  aks6d1c7lem1  42757  aks5lem1  42763  aks5lem2  42764  aks5lem5a  42768  frlmpwfi  43635  isnumbasgrplem3  43642  mendlmod  43726  idomodle  43728  2zrng0  48826  cznabel  48842  cznrng  48843  crhmsubcALTV  48909  fldcatALTV  48913  fldhmsubcALTV  48915  mgpsumz  48944  mgpsumn  48945  evl1at0  48973  evl1at1  48974