Theorem crngring 19804

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6437  CMndccmn 19395  mulGrpcmgp 19729  Ringcrg 19792  CRingccrg 19793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-cring 19795

This theorem is referenced by:  crngringd  19805  gsummgp0  19856  prdscrngd  19861  crngbinom  19869  dvdsunit  19914  unitmulclb  19916  unitabl  19919  idsrngd  20131  rmodislmod  20200  rmodislmodOLD  20201  quscrng  20520  cnring  20629  zringring  20682  zring0  20689  znzrh2  20762  zncyg  20765  zndvds0  20767  znf1o  20768  zzngim  20769  znfld  20777  znchr  20779  znunit  20780  znrrg  20782  cygznlem3  20786  re0g  20826  assa2ass  21079  sraassa  21083  rlmassa  21084  assamulgscmlem2  21113  psrcrng  21191  psrassa  21192  mplcrng  21235  mplassa  21236  mplcoe2  21251  mplbas2  21252  mplmon2mul  21286  mplind  21287  evlslem2  21298  evlslem3  21299  evlslem6  21300  evlseu  21302  evlsval2  21306  evlsgsumadd  21310  evlsgsummul  21311  evlrhm  21315  evlsscasrng  21316  evlsca  21317  evlsvarsrng  21318  evlvar  21319  mpfind  21326  ply1crng  21378  ply1assa  21379  lply1binom  21486  lply1binomsc  21487  evls1rhmlem  21496  evls1gsumadd  21499  evls1gsummul  21500  evl1val  21504  evl1sca  21509  evl1scad  21510  evl1var  21511  evl1vard  21512  evls1var  21513  evls1scasrng  21514  evls1varsrng  21515  evl1subd  21517  evl1expd  21520  pf1const  21521  pf1id  21522  pf1ind  21530  evl1gsumdlem  21531  evl1gsumd  21532  evl1gsumadd  21533  evl1gsummul  21535  evl1varpw  21536  evl1scvarpw  21538  evl1scvarpwval  21539  evl1gsummon  21540  mamuvs2  21562  matassa  21602  madetsumid  21619  madetsmelbas  21622  madetsmelbas2  21623  mat1dimcrng  21635  dmatcrng  21660  scmatcrng  21679  mdetleib2  21746  mdetf  21753  m1detdiag  21755  mdetdiaglem  21756  mdetdiag  21757  mdet1  21759  mdetrlin  21760  mdetrsca  21761  mdetrsca2  21762  mdetr0  21763  mdet0  21764  mdetrlin2  21765  mdetralt  21766  mdetero  21768  mdetmul  21781  maducoeval2  21798  maduf  21799  madutpos  21800  madugsum  21801  madurid  21802  madulid  21803  marep01ma  21818  smadiadetlem0  21819  smadiadetlem1a  21821  smadiadetlem3lem2  21825  smadiadetlem3  21826  smadiadetlem4  21827  smadiadet  21828  smadiadetglem1  21829  smadiadetglem2  21830  smadiadetg  21831  matinv  21835  matunit  21836  slesolinv  21838  slesolinvbi  21839  slesolex  21840  cramerimplem1  21841  cramerimplem2  21842  cramerimplem3  21843  cramerimp  21844  cramer  21849  mat2pmatmul  21889  mat2pmatmhm  21891  mat2pmatrhm  21892  mat2pmatlin  21893  m2cpmmhm  21903  m2cpmrhm  21904  m2pmfzgsumcl  21906  m2cpmrngiso  21916  monmatcollpw  21937  pmatcollpwlem  21938  pmatcollpw  21939  pmatcollpwfi  21940  pmatcollpw3fi1lem2  21945  pmatcollpwscmat  21949  monmat2matmon  21982  pm2mp  21983  chpmatply1  21990  chpmat1d  21994  chpdmat  21999  chpscmat  22000  chpscmatgsumbin  22002  chpscmatgsummon  22003  chp0mat  22004  chpidmat  22005  chmaidscmat  22006  chfacfscmulcl  22015  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmulcl  22019  chfacfpmmul0  22020  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmadurid  22025  cpmidgsumm2pm  22027  cpmidpmatlem2  22029  cpmidpmatlem3  22030  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  cpmadugsumfi  22035  cpmidgsum2  22037  cpmadumatpolylem1  22039  cpmadumatpolylem2  22040  cpmadumatpoly  22041  cayhamlem2  22042  chcoeffeqlem  22043  cayhamlem4  22046  cayleyhamilton0  22047  cayleyhamiltonALT  22049  cayleyhamilton1  22050  recvsOLD  24319  fta1glem1  25339  fta1g  25341  fta1blem  25342  dchrelbas3  26395  dchrelbasd  26396  dchrzrh1  26401  dchrzrhmul  26403  dchrmulcl  26406  dchrn0  26407  dchrfi  26412  dchrghm  26413  dchrabs  26417  dchrinv  26418  dchrptlem1  26421  dchrptlem2  26422  dchrptlem3  26423  dchrsum2  26425  dchrhash  26428  sum2dchr  26431  lgsqrlem1  26503  lgsqrlem2  26504  lgsqrlem3  26505  lgsqrlem4  26506  lgsdchr  26512  lgseisenlem3  26534  lgseisenlem4  26535  dchrisum0flblem1  26665  dchrisum0re  26670  freshmansdream  31493  rdivmuldivd  31497  subofld  31524  ringlsmss1  31593  isprmidlc  31632  prmidl0  31635  qsidomlem1  31637  qsidomlem2  31638  mxidlprm  31649  idlsrgmulrss1  31665  ply1chr  31678  mdetpmtr1  31782  mdetpmtr12  31784  madjusmdetlem1  31786  madjusmdetlem4  31789  mdetlap  31791  zarcls1  31828  zarclsint  31831  zarclssn  31832  zartopn  31834  zart0  31838  zarcmplem  31840  rspectps  31842  selvval2lem4  40235  selvval2lem5  40236  frlmpwfi  40930  isnumbasgrplem3  40937  mendlmod  41025  idomrootle  41027  idomodle  41028  2zrng0  45507  cznabel  45523  cznrng  45524  crhmsubc  45647  fldcat  45651  fldhmsubc  45653  crhmsubcALTV  45665  fldcatALTV  45669  fldhmsubcALTV  45671  mgpsumz  45709  mgpsumn  45710  evl1at0  45743  evl1at1  45744