Theorem crngring 20148

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6486  CMndccmn 19677  mulGrpcmgp 20043  Ringcrg 20136  CRingccrg 20137

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-cring 20139

This theorem is referenced by:  crngringd  20149  gsummgp0  20221  prdscrngd  20225  crngbinom  20238  dvdsunit  20282  unitmulclb  20284  unitabl  20287  rdivmuldivd  20316  crhmsubc  20585  fldcat  20686  fldhmsubc  20688  idsrngd  20759  subofld  20780  rmodislmod  20851  quscrng  21208  cnring  21315  zringring  21374  zring0  21383  znzrh2  21470  zncyg  21473  zndvds0  21475  znf1o  21476  zzngim  21477  znfld  21485  znchr  21487  znunit  21488  znrrg  21490  cygznlem3  21494  freshmansdream  21499  re0g  21537  sraassa  21794  sraassaOLD  21795  rlmassa  21796  psrcrng  21897  mplcrng  21946  mplassa  21947  mplcoe2  21964  mplbas2  21965  mplmon2mul  21992  mplind  21993  evlslem2  22002  evlslem3  22003  evlslem6  22004  evlseu  22006  evlsval2  22010  evlsgsumadd  22014  evlsgsummul  22015  evlrhm  22019  evlsscasrng  22020  evlsca  22021  evlsvarsrng  22022  evlvar  22023  mpfind  22030  ply1crng  22099  ply1assa  22100  ply1chr  22209  lply1binom  22213  lply1binomsc  22214  evls1rhmlem  22224  evls1gsumadd  22227  evls1gsummul  22228  evl1val  22232  evl1sca  22237  evl1scad  22238  evl1var  22239  evl1vard  22240  evls1var  22241  evls1scasrng  22242  evls1varsrng  22243  evl1subd  22245  evl1expd  22248  pf1const  22249  pf1id  22250  pf1ind  22258  evl1gsumdlem  22259  evl1gsumd  22260  evl1gsumadd  22261  evl1gsummul  22263  evl1varpw  22264  evl1scvarpw  22266  evl1scvarpwval  22267  evl1gsummon  22268  evls1vsca  22276  mamuvs2  22309  matassa  22347  madetsumid  22364  madetsmelbas  22367  madetsmelbas2  22368  mat1dimcrng  22380  dmatcrng  22405  scmatcrng  22424  mdetleib2  22491  mdetf  22498  m1detdiag  22500  mdetdiaglem  22501  mdetdiag  22502  mdet1  22504  mdetrlin  22505  mdetrsca2  22507  mdetr0  22508  mdet0  22509  mdetrlin2  22510  mdetralt  22511  mdetero  22513  mdetmul  22526  maducoeval2  22543  maduf  22544  madutpos  22545  madugsum  22546  madurid  22547  madulid  22548  marep01ma  22563  smadiadetlem0  22564  smadiadetlem1a  22566  smadiadetlem3lem2  22570  smadiadetlem3  22571  smadiadetlem4  22572  smadiadet  22573  smadiadetglem1  22574  smadiadetglem2  22575  smadiadetg  22576  matinv  22580  matunit  22581  slesolinv  22583  slesolinvbi  22584  slesolex  22585  cramerimplem1  22586  cramerimplem2  22587  cramerimplem3  22588  cramerimp  22589  cramer  22594  mat2pmatmul  22634  mat2pmatmhm  22636  mat2pmatrhm  22637  mat2pmatlin  22638  m2cpmmhm  22648  m2cpmrhm  22649  m2pmfzgsumcl  22651  m2cpmrngiso  22661  monmatcollpw  22682  pmatcollpwlem  22683  pmatcollpw  22684  pmatcollpwfi  22685  pmatcollpw3fi1lem2  22690  pmatcollpwscmat  22694  monmat2matmon  22727  pm2mp  22728  chpmatply1  22735  chpmat1d  22739  chpdmat  22744  chpscmat  22745  chpscmatgsumbin  22747  chpscmatgsummon  22748  chp0mat  22749  chpidmat  22750  chmaidscmat  22751  chfacfscmulcl  22760  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmulcl  22764  chfacfpmmul0  22765  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmadurid  22770  cpmidgsumm2pm  22772  cpmidpmatlem2  22774  cpmidpmatlem3  22775  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cpmadugsumfi  22780  cpmidgsum2  22782  cpmadumatpolylem1  22784  cpmadumatpolylem2  22785  cpmadumatpoly  22786  cayhamlem2  22787  chcoeffeqlem  22788  cayhamlem4  22791  cayleyhamilton0  22792  cayleyhamiltonALT  22794  cayleyhamilton1  22795  fta1glem1  26089  fta1g  26091  fta1blem  26092  idomrootle  26094  dchrelbas3  27165  dchrelbasd  27166  dchrzrh1  27171  dchrzrhmul  27173  dchrmulcl  27176  dchrn0  27177  dchrfi  27182  dchrghm  27183  dchrabs  27187  dchrinv  27188  dchrptlem1  27191  dchrptlem2  27192  dchrptlem3  27193  dchrsum2  27195  dchrhash  27198  sum2dchr  27201  lgsqrlem1  27273  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  lgsdchr  27282  lgseisenlem3  27304  lgseisenlem4  27305  dchrisum0flblem1  27435  dchrisum0re  27440  unitprodclb  33339  ringlsmss1  33346  isprmidlc  33397  prmidl0  33400  qsidomlem1  33402  qsidomlem2  33403  crngmxidl  33419  mxidlprm  33420  idlsrgmulrss1  33461  mdetpmtr1  33792  mdetpmtr12  33794  madjusmdetlem1  33796  madjusmdetlem4  33799  mdetlap  33801  zarcls1  33838  zarclsint  33841  zarclssn  33842  zartopn  33844  zart0  33848  zarcmplem  33850  rspectps  33852  aks6d1c1p2  42085  aks6d1c1p7  42089  aks6d1c1p6  42090  aks6d1c1  42092  hashscontpowcl  42096  hashscontpow  42098  aks6d1c4  42100  aks6d1c2lem3  42102  aks6d1c2  42106  aks6d1c5lem1  42112  aks6d1c5lem3  42113  aks6d1c6lem1  42146  aks6d1c6lem3  42148  aks6d1c6lem5  42153  aks6d1c7lem1  42156  aks5lem1  42162  aks5lem2  42163  aks5lem5a  42167  frlmpwfi  43074  isnumbasgrplem3  43081  mendlmod  43165  idomodle  43167  2zrng0  48232  cznabel  48248  cznrng  48249  crhmsubcALTV  48315  fldcatALTV  48319  fldhmsubcALTV  48321  mgpsumz  48350  mgpsumn  48351  evl1at0  48380  evl1at1  48381