Theorem crngring 19710

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  CMndccmn 19301  mulGrpcmgp 19635  Ringcrg 19698  CRingccrg 19699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-cring 19701

This theorem is referenced by:  crngringd  19711  gsummgp0  19762  prdscrngd  19767  crngbinom  19775  dvdsunit  19820  unitmulclb  19822  unitabl  19825  idsrngd  20037  rmodislmod  20106  rmodislmodOLD  20107  quscrng  20424  cnring  20532  zringring  20585  zring0  20592  znzrh2  20665  zncyg  20668  zndvds0  20670  znf1o  20671  zzngim  20672  znfld  20680  znchr  20682  znunit  20683  znrrg  20685  cygznlem3  20689  re0g  20729  assa2ass  20980  sraassa  20984  rlmassa  20985  assamulgscmlem2  21014  psrcrng  21092  psrassa  21093  mplcrng  21136  mplassa  21137  mplcoe2  21152  mplbas2  21153  mplmon2mul  21187  mplind  21188  evlslem2  21199  evlslem3  21200  evlslem6  21201  evlseu  21203  evlsval2  21207  evlsgsumadd  21211  evlsgsummul  21212  evlrhm  21216  evlsscasrng  21217  evlsca  21218  evlsvarsrng  21219  evlvar  21220  mpfind  21227  ply1crng  21279  ply1assa  21280  lply1binom  21387  lply1binomsc  21388  evls1rhmlem  21397  evls1gsumadd  21400  evls1gsummul  21401  evl1val  21405  evl1sca  21410  evl1scad  21411  evl1var  21412  evl1vard  21413  evls1var  21414  evls1scasrng  21415  evls1varsrng  21416  evl1subd  21418  evl1expd  21421  pf1const  21422  pf1id  21423  pf1ind  21431  evl1gsumdlem  21432  evl1gsumd  21433  evl1gsumadd  21434  evl1gsummul  21436  evl1varpw  21437  evl1scvarpw  21439  evl1scvarpwval  21440  evl1gsummon  21441  mamuvs2  21463  matassa  21501  madetsumid  21518  madetsmelbas  21521  madetsmelbas2  21522  mat1dimcrng  21534  dmatcrng  21559  scmatcrng  21578  mdetleib2  21645  mdetf  21652  m1detdiag  21654  mdetdiaglem  21655  mdetdiag  21656  mdet1  21658  mdetrlin  21659  mdetrsca  21660  mdetrsca2  21661  mdetr0  21662  mdet0  21663  mdetrlin2  21664  mdetralt  21665  mdetero  21667  mdetmul  21680  maducoeval2  21697  maduf  21698  madutpos  21699  madugsum  21700  madurid  21701  madulid  21702  marep01ma  21717  smadiadetlem0  21718  smadiadetlem1a  21720  smadiadetlem3lem2  21724  smadiadetlem3  21725  smadiadetlem4  21726  smadiadet  21727  smadiadetglem1  21728  smadiadetglem2  21729  smadiadetg  21730  matinv  21734  matunit  21735  slesolinv  21737  slesolinvbi  21738  slesolex  21739  cramerimplem1  21740  cramerimplem2  21741  cramerimplem3  21742  cramerimp  21743  cramer  21748  mat2pmatmul  21788  mat2pmatmhm  21790  mat2pmatrhm  21791  mat2pmatlin  21792  m2cpmmhm  21802  m2cpmrhm  21803  m2pmfzgsumcl  21805  m2cpmrngiso  21815  monmatcollpw  21836  pmatcollpwlem  21837  pmatcollpw  21838  pmatcollpwfi  21839  pmatcollpw3fi1lem2  21844  pmatcollpwscmat  21848  monmat2matmon  21881  pm2mp  21882  chpmatply1  21889  chpmat1d  21893  chpdmat  21898  chpscmat  21899  chpscmatgsumbin  21901  chpscmatgsummon  21902  chp0mat  21903  chpidmat  21904  chmaidscmat  21905  chfacfscmulcl  21914  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmulcl  21918  chfacfpmmul0  21919  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadurid  21924  cpmidgsumm2pm  21926  cpmidpmatlem2  21928  cpmidpmatlem3  21929  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmidgsum2  21936  cpmadumatpolylem1  21938  cpmadumatpolylem2  21939  cpmadumatpoly  21940  cayhamlem2  21941  chcoeffeqlem  21942  cayhamlem4  21945  cayleyhamilton0  21946  cayleyhamiltonALT  21948  cayleyhamilton1  21949  recvs  24215  fta1glem1  25235  fta1g  25237  fta1blem  25238  dchrelbas3  26291  dchrelbasd  26292  dchrzrh1  26297  dchrzrhmul  26299  dchrmulcl  26302  dchrn0  26303  dchrfi  26308  dchrghm  26309  dchrabs  26313  dchrinv  26314  dchrptlem1  26317  dchrptlem2  26318  dchrptlem3  26319  dchrsum2  26321  dchrhash  26324  sum2dchr  26327  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  lgsdchr  26408  lgseisenlem3  26430  lgseisenlem4  26431  dchrisum0flblem1  26561  dchrisum0re  26566  freshmansdream  31386  rdivmuldivd  31390  subofld  31417  ringlsmss1  31486  isprmidlc  31525  prmidl0  31528  qsidomlem1  31530  qsidomlem2  31531  mxidlprm  31542  idlsrgmulrss1  31558  ply1chr  31571  mdetpmtr1  31675  mdetpmtr12  31677  madjusmdetlem1  31679  madjusmdetlem4  31682  mdetlap  31684  zarcls1  31721  zarclsint  31724  zarclssn  31725  zartopn  31727  zart0  31731  zarcmplem  31733  rspectps  31735  selvval2lem4  40154  selvval2lem5  40155  frlmpwfi  40839  isnumbasgrplem3  40846  mendlmod  40934  idomrootle  40936  idomodle  40937  2zrng0  45384  cznabel  45400  cznrng  45401  crhmsubc  45524  fldcat  45528  fldhmsubc  45530  crhmsubcALTV  45542  fldcatALTV  45546  fldhmsubcALTV  45548  mgpsumz  45586  mgpsumn  45587  evl1at0  45620  evl1at1  45621