Theorem crngring 20061

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6540  CMndccmn 19642  mulGrpcmgp 19981  Ringcrg 20049  CRingccrg 20050

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-cring 20052

This theorem is referenced by:  crngringd  20062  gsummgp0  20123  prdscrngd  20128  crngbinom  20140  dvdsunit  20185  unitmulclb  20187  unitabl  20190  rdivmuldivd  20219  idsrngd  20462  rmodislmod  20532  rmodislmodOLD  20533  quscrng  20870  cnring  20959  zringring  21012  zring0  21019  znzrh2  21092  zncyg  21095  zndvds0  21097  znf1o  21098  zzngim  21099  znfld  21107  znchr  21109  znunit  21110  znrrg  21112  cygznlem3  21116  re0g  21156  sraassa  21414  sraassaOLD  21415  rlmassa  21416  psrcrng  21524  mplcrng  21571  mplassa  21572  mplcoe2  21587  mplbas2  21588  mplmon2mul  21621  mplind  21622  evlslem2  21633  evlslem3  21634  evlslem6  21635  evlseu  21637  evlsval2  21641  evlsgsumadd  21645  evlsgsummul  21646  evlrhm  21650  evlsscasrng  21651  evlsca  21652  evlsvarsrng  21653  evlvar  21654  mpfind  21661  ply1crng  21713  ply1assa  21714  lply1binom  21821  lply1binomsc  21822  evls1rhmlem  21831  evls1gsumadd  21834  evls1gsummul  21835  evl1val  21839  evl1sca  21844  evl1scad  21845  evl1var  21846  evl1vard  21847  evls1var  21848  evls1scasrng  21849  evls1varsrng  21850  evl1subd  21852  evl1expd  21855  pf1const  21856  pf1id  21857  pf1ind  21865  evl1gsumdlem  21866  evl1gsumd  21867  evl1gsumadd  21868  evl1gsummul  21870  evl1varpw  21871  evl1scvarpw  21873  evl1scvarpwval  21874  evl1gsummon  21875  mamuvs2  21897  matassa  21937  madetsumid  21954  madetsmelbas  21957  madetsmelbas2  21958  mat1dimcrng  21970  dmatcrng  21995  scmatcrng  22014  mdetleib2  22081  mdetf  22088  m1detdiag  22090  mdetdiaglem  22091  mdetdiag  22092  mdet1  22094  mdetrlin  22095  mdetrsca2  22097  mdetr0  22098  mdet0  22099  mdetrlin2  22100  mdetralt  22101  mdetero  22103  mdetmul  22116  maducoeval2  22133  maduf  22134  madutpos  22135  madugsum  22136  madurid  22137  madulid  22138  marep01ma  22153  smadiadetlem0  22154  smadiadetlem1a  22156  smadiadetlem3lem2  22160  smadiadetlem3  22161  smadiadetlem4  22162  smadiadet  22163  smadiadetglem1  22164  smadiadetglem2  22165  smadiadetg  22166  matinv  22170  matunit  22171  slesolinv  22173  slesolinvbi  22174  slesolex  22175  cramerimplem1  22176  cramerimplem2  22177  cramerimplem3  22178  cramerimp  22179  cramer  22184  mat2pmatmul  22224  mat2pmatmhm  22226  mat2pmatrhm  22227  mat2pmatlin  22228  m2cpmmhm  22238  m2cpmrhm  22239  m2pmfzgsumcl  22241  m2cpmrngiso  22251  monmatcollpw  22272  pmatcollpwlem  22273  pmatcollpw  22274  pmatcollpwfi  22275  pmatcollpw3fi1lem2  22280  pmatcollpwscmat  22284  monmat2matmon  22317  pm2mp  22318  chpmatply1  22325  chpmat1d  22329  chpdmat  22334  chpscmat  22335  chpscmatgsumbin  22337  chpscmatgsummon  22338  chp0mat  22339  chpidmat  22340  chmaidscmat  22341  chfacfscmulcl  22350  chfacfscmul0  22351  chfacfscmulgsum  22353  chfacfpmmulcl  22354  chfacfpmmul0  22355  chfacfpmmulgsum  22357  chfacfpmmulgsum2  22358  cayhamlem1  22359  cpmadurid  22360  cpmidgsumm2pm  22362  cpmidpmatlem2  22364  cpmidpmatlem3  22365  cpmadugsumlemB  22367  cpmadugsumlemC  22368  cpmadugsumlemF  22369  cpmadugsumfi  22370  cpmidgsum2  22372  cpmadumatpolylem1  22374  cpmadumatpolylem2  22375  cpmadumatpoly  22376  cayhamlem2  22377  chcoeffeqlem  22378  cayhamlem4  22381  cayleyhamilton0  22382  cayleyhamiltonALT  22384  cayleyhamilton1  22385  recvsOLD  24654  fta1glem1  25674  fta1g  25676  fta1blem  25677  dchrelbas3  26730  dchrelbasd  26731  dchrzrh1  26736  dchrzrhmul  26738  dchrmulcl  26741  dchrn0  26742  dchrfi  26747  dchrghm  26748  dchrabs  26752  dchrinv  26753  dchrptlem1  26756  dchrptlem2  26757  dchrptlem3  26758  dchrsum2  26760  dchrhash  26763  sum2dchr  26766  lgsqrlem1  26838  lgsqrlem2  26839  lgsqrlem3  26840  lgsqrlem4  26841  lgsdchr  26847  lgseisenlem3  26869  lgseisenlem4  26870  dchrisum0flblem1  27000  dchrisum0re  27005  freshmansdream  32369  subofld  32422  ringlsmss1  32494  isprmidlc  32554  prmidl0  32557  qsidomlem1  32559  qsidomlem2  32560  crngmxidl  32573  mxidlprm  32574  idlsrgmulrss1  32613  evls1vsca  32638  ply1chr  32649  mdetpmtr1  32791  mdetpmtr12  32793  madjusmdetlem1  32795  madjusmdetlem4  32798  mdetlap  32800  zarcls1  32837  zarclsint  32840  zarclssn  32841  zartopn  32843  zart0  32847  zarcmplem  32849  rspectps  32851  selvcllem5  41151  frlmpwfi  41825  isnumbasgrplem3  41832  mendlmod  41920  idomrootle  41922  idomodle  41923  2zrng0  46789  cznabel  46805  cznrng  46806  crhmsubc  46929  fldcat  46933  fldhmsubc  46935  crhmsubcALTV  46947  fldcatALTV  46951  fldhmsubcALTV  46953  mgpsumz  46991  mgpsumn  46992  evl1at0  47025  evl1at1  47026