Theorem crngring 18381

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

Syntax hints:   → wi 4   ∈ wcel 1977  ‘cfv 5804  CMndccmn 18016  mulGrpcmgp 18312  Ringcrg 18370  CRingccrg 18371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-cring 18373

This theorem is referenced by:  gsummgp0  18431  prdscrngd  18436  crngbinom  18444  dvdsunit  18486  unitmulclb  18488  unitabl  18491  idsrngd  18685  quscrng  19061  assa2ass  19143  sraassa  19146  rlmassa  19147  asclrhm  19163  assamulgscmlem2  19170  psrcrng  19234  psrassa  19235  mplcrng  19274  mplassa  19275  mplcoe2  19290  mplbas2  19291  mplmon2mul  19322  mplind  19323  evlslem2  19333  evlslem6  19334  evlslem3  19335  evlslem1  19336  evlseu  19337  evlsval2  19341  evlrhm  19346  evlsscasrng  19347  evlsca  19348  evlsvarsrng  19349  evlvar  19350  mpfind  19357  ply1crng  19389  ply1assa  19390  lply1binom  19497  lply1binomsc  19498  evls1rhmlem  19507  evls1gsumadd  19510  evls1gsummul  19511  evl1val  19514  evl1sca  19519  evl1scad  19520  evl1var  19521  evl1vard  19522  evls1var  19523  evls1scasrng  19524  evls1varsrng  19525  evl1subd  19527  evl1expd  19530  pf1const  19531  pf1id  19532  pf1ind  19540  evl1gsumdlem  19541  evl1gsumd  19542  evl1gsumadd  19543  evl1gsummul  19545  evl1varpw  19546  evl1scvarpw  19548  evl1scvarpwval  19549  evl1gsummon  19550  cnring  19587  zringring  19640  zring0  19647  znzrh2  19713  zncyg  19716  zndvds0  19718  znf1o  19719  zzngim  19720  znfld  19728  znchr  19730  znunit  19731  znrrg  19733  cygznlem3  19737  re0g  19777  mamuvs2  20031  matassa  20069  madetsumid  20086  madetsmelbas  20089  madetsmelbas2  20090  mat1dimcrng  20102  dmatcrng  20127  scmatcrng  20146  mdetleib2  20213  mdetf  20220  m1detdiag  20222  mdetdiaglem  20223  mdetdiag  20224  mdet1  20226  mdetrlin  20227  mdetrsca  20228  mdetrsca2  20229  mdetr0  20230  mdet0  20231  mdetrlin2  20232  mdetralt  20233  mdetero  20235  mdetmul  20248  maducoeval2  20265  maduf  20266  madutpos  20267  madugsum  20268  madurid  20269  madulid  20270  marep01ma  20285  smadiadetlem0  20286  smadiadetlem1a  20288  smadiadetlem3lem2  20292  smadiadetlem3  20293  smadiadetlem4  20294  smadiadet  20295  smadiadetglem1  20296  smadiadetglem2  20297  smadiadetg  20298  matinv  20302  matunit  20303  slesolinv  20305  slesolinvbi  20306  slesolex  20307  cramerimplem1  20308  cramerimplem2  20309  cramerimplem3  20310  cramerimp  20311  cramer  20316  mat2pmatmul  20355  mat2pmatmhm  20357  mat2pmatrhm  20358  mat2pmatlin  20359  m2cpmmhm  20369  m2cpmrhm  20370  m2pmfzgsumcl  20372  m2cpmrngiso  20382  monmatcollpw  20403  pmatcollpwlem  20404  pmatcollpw  20405  pmatcollpwfi  20406  pmatcollpw3fi1lem2  20411  pmatcollpwscmat  20415  monmat2matmon  20448  pm2mp  20449  chpmatply1  20456  chpmat1d  20460  chpdmat  20465  chpscmat  20466  chpscmatgsumbin  20468  chpscmatgsummon  20469  chp0mat  20470  chpidmat  20471  chmaidscmat  20472  chfacfscmulcl  20481  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmulcl  20485  chfacfpmmul0  20486  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmadurid  20491  cpmidgsumm2pm  20493  cpmidpmatlem2  20495  cpmidpmatlem3  20496  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmidgsum2  20503  cpmadumatpolylem1  20505  cpmadumatpolylem2  20506  cpmadumatpoly  20507  cayhamlem2  20508  chcoeffeqlem  20509  cayhamlem4  20512  cayleyhamilton0  20513  cayleyhamiltonALT  20515  cayleyhamilton1  20516  recvs  22754  fta1glem1  23729  fta1g  23731  fta1blem  23732  dchrelbas3  24763  dchrelbasd  24764  dchrzrh1  24769  dchrzrhmul  24771  dchrmulcl  24774  dchrn0  24775  dchrfi  24780  dchrghm  24781  dchrabs  24785  dchrinv  24786  dchrptlem1  24789  dchrptlem2  24790  dchrptlem3  24791  dchrsum2  24793  dchrhash  24796  sum2dchr  24799  lgsqrlem1  24871  lgsqrlem2  24872  lgsqrlem3  24873  lgsqrlem4  24874  lgsdchr  24880  lgseisenlem3  24902  lgseisenlem4  24903  dchrisum0flblem1  24997  dchrisum0re  25002  rdivmuldivd  29122  subofld  29147  mdetpmtr1  29217  mdetpmtr12  29219  madjusmdetlem1  29221  madjusmdetlem4  29224  mdetlap  29226  frlmpwfi  36686  isnumbasgrplem3  36694  mendlmod  36782  idomrootle  36792  idomodle  36793  2zrng0  41728  cznabel  41746  cznrng  41747  crhmsubc  41870  fldcat  41874  fldhmsubc  41876  crhmsubcALTV  41889  fldcatALTV  41893  fldhmsubcALTV  41895  mgpsumz  41934  mgpsumn  41935  evl1at0  41973  evl1at1  41974