Theorem crngring 19990

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6501  CMndccmn 19576  mulGrpcmgp 19910  Ringcrg 19978  CRingccrg 19979

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-cring 19981

This theorem is referenced by:  crngringd  19991  gsummgp0  20046  prdscrngd  20051  crngbinom  20061  dvdsunit  20106  unitmulclb  20108  unitabl  20111  rdivmuldivd  20138  idsrngd  20377  rmodislmod  20447  rmodislmodOLD  20448  quscrng  20769  cnring  20856  zringring  20909  zring0  20916  znzrh2  20989  zncyg  20992  zndvds0  20994  znf1o  20995  zzngim  20996  znfld  21004  znchr  21006  znunit  21007  znrrg  21009  cygznlem3  21013  re0g  21053  sraassa  21310  rlmassa  21311  psrcrng  21419  mplcrng  21463  mplassa  21464  mplcoe2  21479  mplbas2  21480  mplmon2mul  21514  mplind  21515  evlslem2  21526  evlslem3  21527  evlslem6  21528  evlseu  21530  evlsval2  21534  evlsgsumadd  21538  evlsgsummul  21539  evlrhm  21543  evlsscasrng  21544  evlsca  21545  evlsvarsrng  21546  evlvar  21547  mpfind  21554  ply1crng  21606  ply1assa  21607  lply1binom  21714  lply1binomsc  21715  evls1rhmlem  21724  evls1gsumadd  21727  evls1gsummul  21728  evl1val  21732  evl1sca  21737  evl1scad  21738  evl1var  21739  evl1vard  21740  evls1var  21741  evls1scasrng  21742  evls1varsrng  21743  evl1subd  21745  evl1expd  21748  pf1const  21749  pf1id  21750  pf1ind  21758  evl1gsumdlem  21759  evl1gsumd  21760  evl1gsumadd  21761  evl1gsummul  21763  evl1varpw  21764  evl1scvarpw  21766  evl1scvarpwval  21767  evl1gsummon  21768  mamuvs2  21790  matassa  21830  madetsumid  21847  madetsmelbas  21850  madetsmelbas2  21851  mat1dimcrng  21863  dmatcrng  21888  scmatcrng  21907  mdetleib2  21974  mdetf  21981  m1detdiag  21983  mdetdiaglem  21984  mdetdiag  21985  mdet1  21987  mdetrlin  21988  mdetrsca  21989  mdetrsca2  21990  mdetr0  21991  mdet0  21992  mdetrlin2  21993  mdetralt  21994  mdetero  21996  mdetmul  22009  maducoeval2  22026  maduf  22027  madutpos  22028  madugsum  22029  madurid  22030  madulid  22031  marep01ma  22046  smadiadetlem0  22047  smadiadetlem1a  22049  smadiadetlem3lem2  22053  smadiadetlem3  22054  smadiadetlem4  22055  smadiadet  22056  smadiadetglem1  22057  smadiadetglem2  22058  smadiadetg  22059  matinv  22063  matunit  22064  slesolinv  22066  slesolinvbi  22067  slesolex  22068  cramerimplem1  22069  cramerimplem2  22070  cramerimplem3  22071  cramerimp  22072  cramer  22077  mat2pmatmul  22117  mat2pmatmhm  22119  mat2pmatrhm  22120  mat2pmatlin  22121  m2cpmmhm  22131  m2cpmrhm  22132  m2pmfzgsumcl  22134  m2cpmrngiso  22144  monmatcollpw  22165  pmatcollpwlem  22166  pmatcollpw  22167  pmatcollpwfi  22168  pmatcollpw3fi1lem2  22173  pmatcollpwscmat  22177  monmat2matmon  22210  pm2mp  22211  chpmatply1  22218  chpmat1d  22222  chpdmat  22227  chpscmat  22228  chpscmatgsumbin  22230  chpscmatgsummon  22231  chp0mat  22232  chpidmat  22233  chmaidscmat  22234  chfacfscmulcl  22243  chfacfscmul0  22244  chfacfscmulgsum  22246  chfacfpmmulcl  22247  chfacfpmmul0  22248  chfacfpmmulgsum  22250  chfacfpmmulgsum2  22251  cayhamlem1  22252  cpmadurid  22253  cpmidgsumm2pm  22255  cpmidpmatlem2  22257  cpmidpmatlem3  22258  cpmadugsumlemB  22260  cpmadugsumlemC  22261  cpmadugsumlemF  22262  cpmadugsumfi  22263  cpmidgsum2  22265  cpmadumatpolylem1  22267  cpmadumatpolylem2  22268  cpmadumatpoly  22269  cayhamlem2  22270  chcoeffeqlem  22271  cayhamlem4  22274  cayleyhamilton0  22275  cayleyhamiltonALT  22277  cayleyhamilton1  22278  recvsOLD  24547  fta1glem1  25567  fta1g  25569  fta1blem  25570  dchrelbas3  26623  dchrelbasd  26624  dchrzrh1  26629  dchrzrhmul  26631  dchrmulcl  26634  dchrn0  26635  dchrfi  26640  dchrghm  26641  dchrabs  26645  dchrinv  26646  dchrptlem1  26649  dchrptlem2  26650  dchrptlem3  26651  dchrsum2  26653  dchrhash  26656  sum2dchr  26659  lgsqrlem1  26731  lgsqrlem2  26732  lgsqrlem3  26733  lgsqrlem4  26734  lgsdchr  26740  lgseisenlem3  26762  lgseisenlem4  26763  dchrisum0flblem1  26893  dchrisum0re  26898  freshmansdream  32137  subofld  32182  ringlsmss1  32250  isprmidlc  32296  prmidl0  32299  qsidomlem1  32301  qsidomlem2  32302  mxidlprm  32313  idlsrgmulrss1  32329  evls1vsca  32352  ply1chr  32360  mdetpmtr1  32493  mdetpmtr12  32495  madjusmdetlem1  32497  madjusmdetlem4  32500  mdetlap  32502  zarcls1  32539  zarclsint  32542  zarclssn  32543  zartopn  32545  zart0  32549  zarcmplem  32551  rspectps  32553  selvcllem5  40818  frlmpwfi  41483  isnumbasgrplem3  41490  mendlmod  41578  idomrootle  41580  idomodle  41581  2zrng0  46356  cznabel  46372  cznrng  46373  crhmsubc  46496  fldcat  46500  fldhmsubc  46502  crhmsubcALTV  46514  fldcatALTV  46518  fldhmsubcALTV  46520  mgpsumz  46558  mgpsumn  46559  evl1at0  46592  evl1at1  46593