Theorem crngring 20350

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6540  CMndccmn 19873  mulGrpcmgp 20239  Ringcrg 20338  CRingccrg 20339

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-cring 20341

This theorem is used by:  crngringd  20351  gsummgp0  20424  prdscrngd  20428  crngbinom  20442  dvdsunit  20486  unitmulclb  20488  unitabl  20491  rdivmuldivd  20520  crhmsubc  20810  fldcat  20915  fldhmsubc  20917  idsrngd  20988  subofld  21009  rmodislmod  21080  isfieldidl  21415  isfieldidl2  21416  df2idl2crng  21450  quscrng  21452  isprmidlc  21501  cmprmidlmcl  21504  prmidl0  21507  qsidomlem1  21509  qsidomlem2  21510  prmidlsubm  21516  cnring  21573  zringring  21628  zring0  21637  znzrh2  21724  zncyg  21727  zndvds0  21729  znf1o  21730  zzngim  21731  znfld  21739  znchr  21741  znunit  21742  znrrg  21744  cygznlem3  21748  freshmansdream  21753  re0g  21791  sraassa  22048  rlmassa  22049  psrcrng  22150  mplcrng  22199  mplassa  22200  mplcoe2  22221  mplbas2  22222  mplmon2mul  22249  mplind  22250  evlslem2  22259  evlslem3  22260  evlslem6  22261  evlseu  22263  evlsval2  22267  evlsgsumadd  22276  evlsgsummul  22277  evlrhm  22281  evlsscasrng  22285  evlsca  22286  evlsvarsrng  22287  evlvar  22288  mpfind  22295  ply1crng  22387  ply1assa  22388  ply1chr  22495  lply1binom  22499  lply1binomsc  22500  evls1rhmlem  22510  evls1gsumadd  22513  evls1gsummul  22514  evl1val  22518  evl1sca  22523  evl1scad  22524  evl1var  22525  evl1vard  22526  evls1var  22527  evls1scasrng  22528  evls1varsrng  22529  evl1subd  22531  evl1expd  22534  pf1const  22535  pf1id  22536  pf1ind  22544  evl1gsumdlem  22545  evl1gsumd  22546  evl1gsumadd  22547  evl1gsummul  22549  evl1varpw  22550  evl1scvarpw  22552  evl1scvarpwval  22553  evl1gsummon  22554  evls1vsca  22562  mamuvs2  22592  matassa  22630  madetsumid  22647  madetsmelbas  22650  madetsmelbas2  22651  mat1dimcrng  22663  dmatcrng  22688  scmatcrng  22707  mdetleib2  22774  mdetf  22781  m1detdiag  22783  mdetdiaglem  22784  mdetdiag  22785  mdet1  22787  mdetrlin  22788  mdetrsca2  22790  mdetr0  22791  mdet0  22792  mdetrlin2  22793  mdetralt  22794  mdetero  22796  mdetmul  22809  maducoeval2  22826  maduf  22827  madutpos  22828  madugsum  22829  madurid  22830  madulid  22831  marep01ma  22846  smadiadetlem0  22847  smadiadetlem1a  22849  smadiadetlem3lem2  22853  smadiadetlem3  22854  smadiadetlem4  22855  smadiadet  22856  smadiadetglem1  22857  smadiadetglem2  22858  smadiadetg  22859  matinv  22863  matunit  22864  slesolinv  22866  slesolinvbi  22867  slesolex  22868  cramerimplem1  22869  cramerimplem2  22870  cramerimplem3  22871  cramerimp  22872  cramer  22877  mat2pmatmul  22917  mat2pmatmhm  22919  mat2pmatrhm  22920  mat2pmatlin  22921  m2cpmmhm  22931  m2cpmrhm  22932  m2pmfzgsumcl  22934  m2cpmrngiso  22944  monmatcollpw  22965  pmatcollpwlem  22966  pmatcollpw  22967  pmatcollpwfi  22968  pmatcollpw3fi1lem2  22973  pmatcollpwscmat  22977  monmat2matmon  23010  pm2mp  23011  chpmatply1  23018  chpmat1d  23022  chpdmat  23027  chpscmat  23028  chpscmatgsumbin  23030  chpscmatgsummon  23031  chp0mat  23032  chpidmat  23033  chmaidscmat  23034  chfacfscmulcl  23043  chfacfscmul0  23044  chfacfscmulgsum  23046  chfacfpmmulcl  23047  chfacfpmmul0  23048  chfacfpmmulgsum  23050  chfacfpmmulgsum2  23051  cayhamlem1  23052  cpmadurid  23053  cpmidgsumm2pm  23055  cpmidpmatlem2  23057  cpmidpmatlem3  23058  cpmadugsumlemB  23060  cpmadugsumlemC  23061  cpmadugsumlemF  23062  cpmadugsumfi  23063  cpmidgsum2  23065  cpmadumatpolylem1  23067  cpmadumatpolylem2  23068  cpmadumatpoly  23069  cayhamlem2  23070  chcoeffeqlem  23071  cayhamlem4  23074  cayleyhamilton0  23075  cayleyhamiltonALT  23077  cayleyhamilton1  23078  fta1glem1  26354  fta1g  26356  fta1blem  26357  idomrootle  26359  dchrelbas3  27431  dchrelbasd  27432  dchrzrh1  27437  dchrzrhmul  27439  dchrmulcl  27442  dchrn0  27443  dchrfi  27448  dchrghm  27449  dchrabs  27453  dchrinv  27454  dchrptlem1  27457  dchrptlem2  27458  dchrptlem3  27459  dchrsum2  27461  dchrhash  27464  sum2dchr  27467  lgsqrlem1  27539  lgsqrlem2  27540  lgsqrlem3  27541  lgsqrlem4  27542  lgsdchr  27548  lgseisenlem3  27570  lgseisenlem4  27571  dchrisum0flblem1  27701  dchrisum0re  27706  unitprodclb  33725  ringlsmss1  33730  crngmxidl  33775  mxidlprm  33776  dflringlem3  33809  dflring3  33810  idlsrgmulrss1  33824  psrmonprod  33965  esplyfvaln  33987  mdetpmtr1  34236  mdetpmtr12  34238  madjusmdetlem1  34240  madjusmdetlem4  34243  mdetlap  34245  zarcls1  34282  zarclsint  34285  zarclssn  34286  zartopn  34288  zart0  34292  zarcmplem  34294  rspectps  34296  aks6d1c1p2  42909  aks6d1c1p7  42913  aks6d1c1p6  42914  aks6d1c1  42916  hashscontpowcl  42920  hashscontpow  42922  aks6d1c4  42924  aks6d1c2lem3  42926  aks6d1c2  42930  aks6d1c5lem1  42936  aks6d1c5lem3  42937  aks6d1c6lem1  42970  aks6d1c6lem3  42972  aks6d1c6lem5  42977  aks6d1c7lem1  42980  aks5lem1  42986  aks5lem2  42987  aks5lem5a  42991  frlmpwfi  43858  isnumbasgrplem3  43865  mendlmod  43949  idomodle  43951  2zrng0  49042  cznabel  49058  cznrng  49059  crhmsubcALTV  49125  fldcatALTV  49129  fldhmsubcALTV  49131  crngprmringidom  49139  isidom3  49143  idomcanl  49145  mgpsumz  49175  mgpsumn  49176  evl1at0  49204  evl1at1  49205