Theorem crngring 20171

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6489  CMndccmn 19700  mulGrpcmgp 20066  Ringcrg 20159  CRingccrg 20160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-cring 20162

This theorem is referenced by:  crngringd  20172  gsummgp0  20244  prdscrngd  20248  crngbinom  20262  dvdsunit  20306  unitmulclb  20308  unitabl  20311  rdivmuldivd  20340  crhmsubc  20606  fldcat  20707  fldhmsubc  20709  idsrngd  20780  subofld  20801  rmodislmod  20872  quscrng  21229  cnring  21336  zringring  21395  zring0  21404  znzrh2  21491  zncyg  21494  zndvds0  21496  znf1o  21497  zzngim  21498  znfld  21506  znchr  21508  znunit  21509  znrrg  21511  cygznlem3  21515  freshmansdream  21520  re0g  21558  sraassa  21815  sraassaOLD  21816  rlmassa  21817  psrcrng  21918  mplcrng  21967  mplassa  21968  mplcoe2  21987  mplbas2  21988  mplmon2mul  22015  mplind  22016  evlslem2  22025  evlslem3  22026  evlslem6  22027  evlseu  22029  evlsval2  22033  evlsgsumadd  22042  evlsgsummul  22043  evlrhm  22047  evlsscasrng  22051  evlsca  22052  evlsvarsrng  22053  evlvar  22054  mpfind  22061  ply1crng  22130  ply1assa  22131  ply1chr  22241  lply1binom  22245  lply1binomsc  22246  evls1rhmlem  22256  evls1gsumadd  22259  evls1gsummul  22260  evl1val  22264  evl1sca  22269  evl1scad  22270  evl1var  22271  evl1vard  22272  evls1var  22273  evls1scasrng  22274  evls1varsrng  22275  evl1subd  22277  evl1expd  22280  pf1const  22281  pf1id  22282  pf1ind  22290  evl1gsumdlem  22291  evl1gsumd  22292  evl1gsumadd  22293  evl1gsummul  22295  evl1varpw  22296  evl1scvarpw  22298  evl1scvarpwval  22299  evl1gsummon  22300  evls1vsca  22308  mamuvs2  22341  matassa  22379  madetsumid  22396  madetsmelbas  22399  madetsmelbas2  22400  mat1dimcrng  22412  dmatcrng  22437  scmatcrng  22456  mdetleib2  22523  mdetf  22530  m1detdiag  22532  mdetdiaglem  22533  mdetdiag  22534  mdet1  22536  mdetrlin  22537  mdetrsca2  22539  mdetr0  22540  mdet0  22541  mdetrlin2  22542  mdetralt  22543  mdetero  22545  mdetmul  22558  maducoeval2  22575  maduf  22576  madutpos  22577  madugsum  22578  madurid  22579  madulid  22580  marep01ma  22595  smadiadetlem0  22596  smadiadetlem1a  22598  smadiadetlem3lem2  22602  smadiadetlem3  22603  smadiadetlem4  22604  smadiadet  22605  smadiadetglem1  22606  smadiadetglem2  22607  smadiadetg  22608  matinv  22612  matunit  22613  slesolinv  22615  slesolinvbi  22616  slesolex  22617  cramerimplem1  22618  cramerimplem2  22619  cramerimplem3  22620  cramerimp  22621  cramer  22626  mat2pmatmul  22666  mat2pmatmhm  22668  mat2pmatrhm  22669  mat2pmatlin  22670  m2cpmmhm  22680  m2cpmrhm  22681  m2pmfzgsumcl  22683  m2cpmrngiso  22693  monmatcollpw  22714  pmatcollpwlem  22715  pmatcollpw  22716  pmatcollpwfi  22717  pmatcollpw3fi1lem2  22722  pmatcollpwscmat  22726  monmat2matmon  22759  pm2mp  22760  chpmatply1  22767  chpmat1d  22771  chpdmat  22776  chpscmat  22777  chpscmatgsumbin  22779  chpscmatgsummon  22780  chp0mat  22781  chpidmat  22782  chmaidscmat  22783  chfacfscmulcl  22792  chfacfscmul0  22793  chfacfscmulgsum  22795  chfacfpmmulcl  22796  chfacfpmmul0  22797  chfacfpmmulgsum  22799  chfacfpmmulgsum2  22800  cayhamlem1  22801  cpmadurid  22802  cpmidgsumm2pm  22804  cpmidpmatlem2  22806  cpmidpmatlem3  22807  cpmadugsumlemB  22809  cpmadugsumlemC  22810  cpmadugsumlemF  22811  cpmadugsumfi  22812  cpmidgsum2  22814  cpmadumatpolylem1  22816  cpmadumatpolylem2  22817  cpmadumatpoly  22818  cayhamlem2  22819  chcoeffeqlem  22820  cayhamlem4  22823  cayleyhamilton0  22824  cayleyhamiltonALT  22826  cayleyhamilton1  22827  fta1glem1  26120  fta1g  26122  fta1blem  26123  idomrootle  26125  dchrelbas3  27196  dchrelbasd  27197  dchrzrh1  27202  dchrzrhmul  27204  dchrmulcl  27207  dchrn0  27208  dchrfi  27213  dchrghm  27214  dchrabs  27218  dchrinv  27219  dchrptlem1  27222  dchrptlem2  27223  dchrptlem3  27224  dchrsum2  27226  dchrhash  27229  sum2dchr  27232  lgsqrlem1  27304  lgsqrlem2  27305  lgsqrlem3  27306  lgsqrlem4  27307  lgsdchr  27313  lgseisenlem3  27335  lgseisenlem4  27336  dchrisum0flblem1  27466  dchrisum0re  27471  unitprodclb  33398  ringlsmss1  33405  isprmidlc  33456  prmidl0  33459  qsidomlem1  33461  qsidomlem2  33462  crngmxidl  33478  mxidlprm  33479  idlsrgmulrss1  33520  mdetpmtr1  33908  mdetpmtr12  33910  madjusmdetlem1  33912  madjusmdetlem4  33915  mdetlap  33917  zarcls1  33954  zarclsint  33957  zarclssn  33958  zartopn  33960  zart0  33964  zarcmplem  33966  rspectps  33968  aks6d1c1p2  42275  aks6d1c1p7  42279  aks6d1c1p6  42280  aks6d1c1  42282  hashscontpowcl  42286  hashscontpow  42288  aks6d1c4  42290  aks6d1c2lem3  42292  aks6d1c2  42296  aks6d1c5lem1  42302  aks6d1c5lem3  42303  aks6d1c6lem1  42336  aks6d1c6lem3  42338  aks6d1c6lem5  42343  aks6d1c7lem1  42346  aks5lem1  42352  aks5lem2  42353  aks5lem5a  42357  frlmpwfi  43255  isnumbasgrplem3  43262  mendlmod  43346  idomodle  43348  2zrng0  48406  cznabel  48422  cznrng  48423  crhmsubcALTV  48489  fldcatALTV  48493  fldhmsubcALTV  48495  mgpsumz  48524  mgpsumn  48525  evl1at0  48553  evl1at1  48554