Theorem crngring 20161

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  CMndccmn 19717  mulGrpcmgp 20056  Ringcrg 20149  CRingccrg 20150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-cring 20152

This theorem is referenced by:  crngringd  20162  gsummgp0  20234  prdscrngd  20238  crngbinom  20251  dvdsunit  20295  unitmulclb  20297  unitabl  20300  rdivmuldivd  20329  crhmsubc  20598  fldcat  20699  fldhmsubc  20701  idsrngd  20772  rmodislmod  20843  quscrng  21200  cnring  21309  zringring  21366  zring0  21375  znzrh2  21462  zncyg  21465  zndvds0  21467  znf1o  21468  zzngim  21469  znfld  21477  znchr  21479  znunit  21480  znrrg  21482  cygznlem3  21486  freshmansdream  21491  re0g  21528  sraassa  21785  sraassaOLD  21786  rlmassa  21787  psrcrng  21888  mplcrng  21937  mplassa  21938  mplcoe2  21955  mplbas2  21956  mplmon2mul  21983  mplind  21984  evlslem2  21993  evlslem3  21994  evlslem6  21995  evlseu  21997  evlsval2  22001  evlsgsumadd  22005  evlsgsummul  22006  evlrhm  22010  evlsscasrng  22011  evlsca  22012  evlsvarsrng  22013  evlvar  22014  mpfind  22021  ply1crng  22090  ply1assa  22091  ply1chr  22200  lply1binom  22204  lply1binomsc  22205  evls1rhmlem  22215  evls1gsumadd  22218  evls1gsummul  22219  evl1val  22223  evl1sca  22228  evl1scad  22229  evl1var  22230  evl1vard  22231  evls1var  22232  evls1scasrng  22233  evls1varsrng  22234  evl1subd  22236  evl1expd  22239  pf1const  22240  pf1id  22241  pf1ind  22249  evl1gsumdlem  22250  evl1gsumd  22251  evl1gsumadd  22252  evl1gsummul  22254  evl1varpw  22255  evl1scvarpw  22257  evl1scvarpwval  22258  evl1gsummon  22259  evls1vsca  22267  mamuvs2  22300  matassa  22338  madetsumid  22355  madetsmelbas  22358  madetsmelbas2  22359  mat1dimcrng  22371  dmatcrng  22396  scmatcrng  22415  mdetleib2  22482  mdetf  22489  m1detdiag  22491  mdetdiaglem  22492  mdetdiag  22493  mdet1  22495  mdetrlin  22496  mdetrsca2  22498  mdetr0  22499  mdet0  22500  mdetrlin2  22501  mdetralt  22502  mdetero  22504  mdetmul  22517  maducoeval2  22534  maduf  22535  madutpos  22536  madugsum  22537  madurid  22538  madulid  22539  marep01ma  22554  smadiadetlem0  22555  smadiadetlem1a  22557  smadiadetlem3lem2  22561  smadiadetlem3  22562  smadiadetlem4  22563  smadiadet  22564  smadiadetglem1  22565  smadiadetglem2  22566  smadiadetg  22567  matinv  22571  matunit  22572  slesolinv  22574  slesolinvbi  22575  slesolex  22576  cramerimplem1  22577  cramerimplem2  22578  cramerimplem3  22579  cramerimp  22580  cramer  22585  mat2pmatmul  22625  mat2pmatmhm  22627  mat2pmatrhm  22628  mat2pmatlin  22629  m2cpmmhm  22639  m2cpmrhm  22640  m2pmfzgsumcl  22642  m2cpmrngiso  22652  monmatcollpw  22673  pmatcollpwlem  22674  pmatcollpw  22675  pmatcollpwfi  22676  pmatcollpw3fi1lem2  22681  pmatcollpwscmat  22685  monmat2matmon  22718  pm2mp  22719  chpmatply1  22726  chpmat1d  22730  chpdmat  22735  chpscmat  22736  chpscmatgsumbin  22738  chpscmatgsummon  22739  chp0mat  22740  chpidmat  22741  chmaidscmat  22742  chfacfscmulcl  22751  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmulcl  22755  chfacfpmmul0  22756  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmadurid  22761  cpmidgsumm2pm  22763  cpmidpmatlem2  22765  cpmidpmatlem3  22766  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  cpmadugsumfi  22771  cpmidgsum2  22773  cpmadumatpolylem1  22775  cpmadumatpolylem2  22776  cpmadumatpoly  22777  cayhamlem2  22778  chcoeffeqlem  22779  cayhamlem4  22782  cayleyhamilton0  22783  cayleyhamiltonALT  22785  cayleyhamilton1  22786  fta1glem1  26080  fta1g  26082  fta1blem  26083  idomrootle  26085  dchrelbas3  27156  dchrelbasd  27157  dchrzrh1  27162  dchrzrhmul  27164  dchrmulcl  27167  dchrn0  27168  dchrfi  27173  dchrghm  27174  dchrabs  27178  dchrinv  27179  dchrptlem1  27182  dchrptlem2  27183  dchrptlem3  27184  dchrsum2  27186  dchrhash  27189  sum2dchr  27192  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  lgsdchr  27273  lgseisenlem3  27295  lgseisenlem4  27296  dchrisum0flblem1  27426  dchrisum0re  27431  subofld  33301  unitprodclb  33367  ringlsmss1  33374  isprmidlc  33425  prmidl0  33428  qsidomlem1  33430  qsidomlem2  33431  crngmxidl  33447  mxidlprm  33448  idlsrgmulrss1  33489  mdetpmtr1  33820  mdetpmtr12  33822  madjusmdetlem1  33824  madjusmdetlem4  33827  mdetlap  33829  zarcls1  33866  zarclsint  33869  zarclssn  33870  zartopn  33872  zart0  33876  zarcmplem  33878  rspectps  33880  aks6d1c1p2  42104  aks6d1c1p7  42108  aks6d1c1p6  42109  aks6d1c1  42111  hashscontpowcl  42115  hashscontpow  42117  aks6d1c4  42119  aks6d1c2lem3  42121  aks6d1c2  42125  aks6d1c5lem1  42131  aks6d1c5lem3  42132  aks6d1c6lem1  42165  aks6d1c6lem3  42167  aks6d1c6lem5  42172  aks6d1c7lem1  42175  aks5lem1  42181  aks5lem2  42182  aks5lem5a  42186  frlmpwfi  43094  isnumbasgrplem3  43101  mendlmod  43185  idomodle  43187  2zrng0  48236  cznabel  48252  cznrng  48253  crhmsubcALTV  48319  fldcatALTV  48323  fldhmsubcALTV  48325  mgpsumz  48354  mgpsumn  48355  evl1at0  48384  evl1at1  48385