Theorem crngring 20465

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 20459	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
3	2	simplbi 502	1 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  CMndccmn 19987  mulGrpcmgp 20353  Ringcrg 20452  CRingccrg 20453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-cring 20455

This theorem is used by:  crngringd  20466  gsummgp0  20540  prdscrngd  20544  crngbinom  20558  dvdsunit  20602  unitmulclb  20604  unitabl  20607  rdivmuldivd  20636  crhmsubc  20927  fldcat  21033  fldhmsubc  21035  idsrngd  21106  subofld  21127  rmodislmod  21198  isfieldidl  21533  isfieldidl2  21534  df2idl2crng  21570  quscrng  21572  isprmidlc  21621  cmprmidlmcl  21624  prmidl0  21627  qsidomlem1  21629  qsidomlem2  21630  prmidlsubm  21636  cnring  21693  zringring  21748  zring0  21757  znzrh2  21844  zncyg  21847  zndvds0  21849  znf1o  21850  zzngim  21851  znfld  21859  znchr  21861  znunit  21862  znrrg  21864  cygznlem3  21868  freshmansdream  21873  re0g  21911  sraassa  22170  rlmassa  22171  psrcrng  22272  mplcrng  22321  mplassa  22322  mplcoe2  22343  mplbas2  22344  mplmon2mul  22371  mplind  22372  evlslem2  22381  evlslem3  22382  evlslem6  22383  evlseu  22385  evlsval2  22389  evlsgsumadd  22398  evlsgsummul  22399  evlrhm  22403  evlsscasrng  22407  evlsca  22408  evlsvarsrng  22409  evlvar  22410  mpfind  22417  ply1crng  22509  ply1assa  22510  ply1chr  22617  lply1binom  22621  lply1binomsc  22622  evls1rhmlem  22632  evls1gsumadd  22635  evls1gsummul  22636  evl1val  22640  evl1sca  22645  evl1scad  22646  evl1var  22647  evl1vard  22648  evls1var  22649  evls1scasrng  22650  evls1varsrng  22651  evl1subd  22653  evl1expd  22656  pf1const  22657  pf1id  22658  pf1ind  22666  evl1gsumdlem  22667  evl1gsumd  22668  evl1gsumadd  22669  evl1gsummul  22671  evl1varpw  22672  evl1scvarpw  22674  evl1scvarpwval  22675  evl1gsummon  22676  evls1vsca  22684  mamuvs2  22714  matassa  22752  madetsumid  22769  madetsmelbas  22772  madetsmelbas2  22773  mat1dimcrng  22785  dmatcrng  22810  scmatcrng  22829  mdetleib2  22896  mdetf  22903  m1detdiag  22905  mdetdiaglem  22906  mdetdiag  22907  mdet1  22909  mdetrlin  22910  mdetrsca2  22912  mdetr0  22913  mdet0  22914  mdetrlin2  22915  mdetralt  22916  mdetero  22918  mdetmul  22931  maducoeval2  22948  maduf  22949  madutpos  22950  madugsum  22951  madurid  22952  madulid  22953  marep01ma  22968  smadiadetlem0  22969  smadiadetlem1a  22971  smadiadetlem3lem2  22975  smadiadetlem3  22976  smadiadetlem4  22977  smadiadet  22978  smadiadetglem1  22979  smadiadetglem2  22980  smadiadetg  22981  matinv  22985  matunit  22986  slesolinv  22991  slesolinvbi  22992  slesolex  22993  cramerimplem1  22994  cramerimplem2  22995  cramerimplem3  22996  cramerimp  22997  cramer  23002  mat2pmatmul  23042  mat2pmatmhm  23044  mat2pmatrhm  23045  mat2pmatlin  23046  m2cpmmhm  23056  m2cpmrhm  23057  m2pmfzgsumcl  23059  m2cpmrngiso  23069  monmatcollpw  23090  pmatcollpwlem  23091  pmatcollpw  23092  pmatcollpwfi  23093  pmatcollpw3fi1lem2  23098  pmatcollpwscmat  23102  monmat2matmon  23135  pm2mp  23136  chpmatply1  23143  chpmat1d  23147  chpdmat  23152  chpscmat  23153  chpscmatgsumbin  23155  chpscmatgsummon  23156  chp0mat  23157  chpidmat  23158  chmaidscmat  23159  chfacfscmulcl  23168  chfacfscmul0  23169  chfacfscmulgsum  23171  chfacfpmmulcl  23172  chfacfpmmul0  23173  chfacfpmmulgsum  23175  chfacfpmmulgsum2  23176  cayhamlem1  23177  cpmadurid  23178  cpmidgsumm2pm  23180  cpmidpmatlem2  23182  cpmidpmatlem3  23183  cpmadugsumlemB  23185  cpmadugsumlemC  23186  cpmadugsumlemF  23187  cpmadugsumfi  23188  cpmidgsum2  23190  cpmadumatpolylem1  23192  cpmadumatpolylem2  23193  cpmadumatpoly  23194  cayhamlem2  23195  chcoeffeqlem  23196  cayhamlem4  23199  cayleyhamilton0  23200  cayleyhamiltonALT  23202  cayleyhamilton1  23203  fta1glem1  26479  fta1g  26481  fta1blem  26482  idomrootle  26484  dchrelbas3  27558  dchrelbasd  27559  dchrzrh1  27564  dchrzrhmul  27566  dchrmulcl  27569  dchrn0  27570  dchrfi  27575  dchrghm  27576  dchrabs  27580  dchrinv  27581  dchrptlem1  27584  dchrptlem2  27585  dchrptlem3  27586  dchrsum2  27588  dchrhash  27591  sum2dchr  27594  lgsqrlem1  27666  lgsqrlem2  27667  lgsqrlem3  27668  lgsqrlem4  27669  lgsdchr  27675  lgseisenlem3  27697  lgseisenlem4  27698  dchrisum0flblem1  27828  dchrisum0re  27833  unitprodclb  33937  ringlsmss1  33942  crngmxidl  33987  mxidlprm  33988  dflringlem3  34021  dflring3  34022  idlsrgmulrss1  34036  psrmonprod  34177  esplyfvaln  34199  mdetpmtr1  34448  mdetpmtr12  34450  madjusmdetlem1  34452  madjusmdetlem4  34455  mdetlap  34457  zarcls1  34494  zarclsint  34497  zarclssn  34498  zartopn  34500  zart0  34504  zarcmplem  34506  rspectps  34508  aks6d1c1p2  43139  aks6d1c1p7  43143  aks6d1c1p6  43144  aks6d1c1  43146  hashscontpowcl  43150  hashscontpow  43152  aks6d1c4  43154  aks6d1c2lem3  43156  aks6d1c2  43160  aks6d1c5lem1  43166  aks6d1c5lem3  43167  aks6d1c6lem1  43200  aks6d1c6lem3  43202  aks6d1c6lem5  43207  aks6d1c7lem1  43210  aks5lem1  43216  aks5lem2  43217  aks5lem5a  43221  frlmpwfi  44084  isnumbasgrplem3  44091  mendlmod  44175  idomodle  44177  2zrng0  49310  cznabel  49326  cznrng  49327  crhmsubcALTV  49393  fldcatALTV  49397  fldhmsubcALTV  49399  crngprmringidom  49407  isidom3  49411  idomcanl  49413  mgpsumz  49443  mgpsumn  49444  evl1at0  49472  evl1at1  49473