Theorem crngring 19302

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6324  CMndccmn 18898  mulGrpcmgp 19232  Ringcrg 19290  CRingccrg 19291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-cring 19293

This theorem is referenced by:  crngringd  19303  gsummgp0  19354  prdscrngd  19359  crngbinom  19367  dvdsunit  19409  unitmulclb  19411  unitabl  19414  idsrngd  19626  rmodislmod  19695  quscrng  20006  cnring  20113  zringring  20166  zring0  20173  znzrh2  20237  zncyg  20240  zndvds0  20242  znf1o  20243  zzngim  20244  znfld  20252  znchr  20254  znunit  20255  znrrg  20257  cygznlem3  20261  re0g  20301  assa2ass  20552  sraassa  20556  rlmassa  20557  ascldimulOLD  20574  asclrhm  20576  assamulgscmlem2  20586  psrcrng  20651  psrassa  20652  mplcrng  20693  mplassa  20694  mplcoe2  20709  mplbas2  20710  mplmon2mul  20740  mplind  20741  evlslem2  20751  evlslem3  20752  evlslem6  20753  evlslem1  20754  evlseu  20755  evlsval2  20759  evlsgsumadd  20763  evlsgsummul  20764  evlrhm  20768  evlsscasrng  20769  evlsca  20770  evlsvarsrng  20771  evlvar  20772  mpfind  20779  ply1crng  20827  ply1assa  20828  lply1binom  20935  lply1binomsc  20936  evls1rhmlem  20945  evls1gsumadd  20948  evls1gsummul  20949  evl1val  20953  evl1sca  20958  evl1scad  20959  evl1var  20960  evl1vard  20961  evls1var  20962  evls1scasrng  20963  evls1varsrng  20964  evl1subd  20966  evl1expd  20969  pf1const  20970  pf1id  20971  pf1ind  20979  evl1gsumdlem  20980  evl1gsumd  20981  evl1gsumadd  20982  evl1gsummul  20984  evl1varpw  20985  evl1scvarpw  20987  evl1scvarpwval  20988  evl1gsummon  20989  mamuvs2  21011  matassa  21049  madetsumid  21066  madetsmelbas  21069  madetsmelbas2  21070  mat1dimcrng  21082  dmatcrng  21107  scmatcrng  21126  mdetleib2  21193  mdetf  21200  m1detdiag  21202  mdetdiaglem  21203  mdetdiag  21204  mdet1  21206  mdetrlin  21207  mdetrsca  21208  mdetrsca2  21209  mdetr0  21210  mdet0  21211  mdetrlin2  21212  mdetralt  21213  mdetero  21215  mdetmul  21228  maducoeval2  21245  maduf  21246  madutpos  21247  madugsum  21248  madurid  21249  madulid  21250  marep01ma  21265  smadiadetlem0  21266  smadiadetlem1a  21268  smadiadetlem3lem2  21272  smadiadetlem3  21273  smadiadetlem4  21274  smadiadet  21275  smadiadetglem1  21276  smadiadetglem2  21277  smadiadetg  21278  matinv  21282  matunit  21283  slesolinv  21285  slesolinvbi  21286  slesolex  21287  cramerimplem1  21288  cramerimplem2  21289  cramerimplem3  21290  cramerimp  21291  cramer  21296  mat2pmatmul  21336  mat2pmatmhm  21338  mat2pmatrhm  21339  mat2pmatlin  21340  m2cpmmhm  21350  m2cpmrhm  21351  m2pmfzgsumcl  21353  m2cpmrngiso  21363  monmatcollpw  21384  pmatcollpwlem  21385  pmatcollpw  21386  pmatcollpwfi  21387  pmatcollpw3fi1lem2  21392  pmatcollpwscmat  21396  monmat2matmon  21429  pm2mp  21430  chpmatply1  21437  chpmat1d  21441  chpdmat  21446  chpscmat  21447  chpscmatgsumbin  21449  chpscmatgsummon  21450  chp0mat  21451  chpidmat  21452  chmaidscmat  21453  chfacfscmulcl  21462  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmulcl  21466  chfacfpmmul0  21467  chfacfpmmulgsum  21469  chfacfpmmulgsum2  21470  cayhamlem1  21471  cpmadurid  21472  cpmidgsumm2pm  21474  cpmidpmatlem2  21476  cpmidpmatlem3  21477  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  cpmadugsumfi  21482  cpmidgsum2  21484  cpmadumatpolylem1  21486  cpmadumatpolylem2  21487  cpmadumatpoly  21488  cayhamlem2  21489  chcoeffeqlem  21490  cayhamlem4  21493  cayleyhamilton0  21494  cayleyhamiltonALT  21496  cayleyhamilton1  21497  recvs  23751  fta1glem1  24766  fta1g  24768  fta1blem  24769  dchrelbas3  25822  dchrelbasd  25823  dchrzrh1  25828  dchrzrhmul  25830  dchrmulcl  25833  dchrn0  25834  dchrfi  25839  dchrghm  25840  dchrabs  25844  dchrinv  25845  dchrptlem1  25848  dchrptlem2  25849  dchrptlem3  25850  dchrsum2  25852  dchrhash  25855  sum2dchr  25858  lgsqrlem1  25930  lgsqrlem2  25931  lgsqrlem3  25932  lgsqrlem4  25933  lgsdchr  25939  lgseisenlem3  25961  lgseisenlem4  25962  dchrisum0flblem1  26092  dchrisum0re  26097  freshmansdream  30909  rdivmuldivd  30913  subofld  30940  ringlsmss1  31003  isprmidlc  31031  prmidl0  31034  qsidomlem1  31036  qsidomlem2  31037  mxidlprm  31048  idlsrgmulrss1  31064  mdetpmtr1  31176  mdetpmtr12  31178  madjusmdetlem1  31180  madjusmdetlem4  31183  mdetlap  31185  zarcls1  31222  zarclsint  31225  zarclssn  31226  zartopn  31228  zart0  31232  zarcmplem  31234  rspectps  31236  selvval2lem4  39431  selvval2lem5  39432  frlmpwfi  40042  isnumbasgrplem3  40049  mendlmod  40137  idomrootle  40139  idomodle  40140  2zrng0  44562  cznabel  44578  cznrng  44579  crhmsubc  44702  fldcat  44706  fldhmsubc  44708  crhmsubcALTV  44720  fldcatALTV  44724  fldhmsubcALTV  44726  mgpsumz  44764  mgpsumn  44765  evl1at0  44799  evl1at1  44800