Theorem crngring 20323

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

Syntax hints:   → wi 4   ∈ wcel 2149  ‘cfv 6533  CMndccmn 19846  mulGrpcmgp 20212  Ringcrg 20311  CRingccrg 20312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-cring 20314

This theorem is referenced by:  crngringd  20324  gsummgp0  20395  prdscrngd  20399  crngbinom  20413  dvdsunit  20457  unitmulclb  20459  unitabl  20462  rdivmuldivd  20491  crhmsubc  20763  fldcat  20860  fldhmsubc  20862  idsrngd  20933  subofld  20954  rmodislmod  21025  df2idl2crng  21388  quscrng  21390  isprmidlc  21439  prmidl0  21443  qsidomlem1  21445  qsidomlem2  21446  prmidlsubm  21452  cnring  21509  zringring  21564  zring0  21573  znzrh2  21660  zncyg  21663  zndvds0  21665  znf1o  21666  zzngim  21667  znfld  21675  znchr  21677  znunit  21678  znrrg  21680  cygznlem3  21684  freshmansdream  21689  re0g  21727  sraassa  21984  rlmassa  21985  psrcrng  22086  mplcrng  22135  mplassa  22136  mplcoe2  22157  mplbas2  22158  mplmon2mul  22185  mplind  22186  evlslem2  22195  evlslem3  22196  evlslem6  22197  evlseu  22199  evlsval2  22203  evlsgsumadd  22212  evlsgsummul  22213  evlrhm  22217  evlsscasrng  22221  evlsca  22222  evlsvarsrng  22223  evlvar  22224  mpfind  22231  ply1crng  22323  ply1assa  22324  ply1chr  22431  lply1binom  22435  lply1binomsc  22436  evls1rhmlem  22446  evls1gsumadd  22449  evls1gsummul  22450  evl1val  22454  evl1sca  22459  evl1scad  22460  evl1var  22461  evl1vard  22462  evls1var  22463  evls1scasrng  22464  evls1varsrng  22465  evl1subd  22467  evl1expd  22470  pf1const  22471  pf1id  22472  pf1ind  22480  evl1gsumdlem  22481  evl1gsumd  22482  evl1gsumadd  22483  evl1gsummul  22485  evl1varpw  22486  evl1scvarpw  22488  evl1scvarpwval  22489  evl1gsummon  22490  evls1vsca  22498  mamuvs2  22528  matassa  22566  madetsumid  22583  madetsmelbas  22586  madetsmelbas2  22587  mat1dimcrng  22599  dmatcrng  22624  scmatcrng  22643  mdetleib2  22710  mdetf  22717  m1detdiag  22719  mdetdiaglem  22720  mdetdiag  22721  mdet1  22723  mdetrlin  22724  mdetrsca2  22726  mdetr0  22727  mdet0  22728  mdetrlin2  22729  mdetralt  22730  mdetero  22732  mdetmul  22745  maducoeval2  22762  maduf  22763  madutpos  22764  madugsum  22765  madurid  22766  madulid  22767  marep01ma  22782  smadiadetlem0  22783  smadiadetlem1a  22785  smadiadetlem3lem2  22789  smadiadetlem3  22790  smadiadetlem4  22791  smadiadet  22792  smadiadetglem1  22793  smadiadetglem2  22794  smadiadetg  22795  matinv  22799  matunit  22800  slesolinv  22802  slesolinvbi  22803  slesolex  22804  cramerimplem1  22805  cramerimplem2  22806  cramerimplem3  22807  cramerimp  22808  cramer  22813  mat2pmatmul  22853  mat2pmatmhm  22855  mat2pmatrhm  22856  mat2pmatlin  22857  m2cpmmhm  22867  m2cpmrhm  22868  m2pmfzgsumcl  22870  m2cpmrngiso  22880  monmatcollpw  22901  pmatcollpwlem  22902  pmatcollpw  22903  pmatcollpwfi  22904  pmatcollpw3fi1lem2  22909  pmatcollpwscmat  22913  monmat2matmon  22946  pm2mp  22947  chpmatply1  22954  chpmat1d  22958  chpdmat  22963  chpscmat  22964  chpscmatgsumbin  22966  chpscmatgsummon  22967  chp0mat  22968  chpidmat  22969  chmaidscmat  22970  chfacfscmulcl  22979  chfacfscmul0  22980  chfacfscmulgsum  22982  chfacfpmmulcl  22983  chfacfpmmul0  22984  chfacfpmmulgsum  22986  chfacfpmmulgsum2  22987  cayhamlem1  22988  cpmadurid  22989  cpmidgsumm2pm  22991  cpmidpmatlem2  22993  cpmidpmatlem3  22994  cpmadugsumlemB  22996  cpmadugsumlemC  22997  cpmadugsumlemF  22998  cpmadugsumfi  22999  cpmidgsum2  23001  cpmadumatpolylem1  23003  cpmadumatpolylem2  23004  cpmadumatpoly  23005  cayhamlem2  23006  chcoeffeqlem  23007  cayhamlem4  23010  cayleyhamilton0  23011  cayleyhamiltonALT  23013  cayleyhamilton1  23014  fta1glem1  26290  fta1g  26292  fta1blem  26293  idomrootle  26295  dchrelbas3  27364  dchrelbasd  27365  dchrzrh1  27370  dchrzrhmul  27372  dchrmulcl  27375  dchrn0  27376  dchrfi  27381  dchrghm  27382  dchrabs  27386  dchrinv  27387  dchrptlem1  27390  dchrptlem2  27391  dchrptlem3  27392  dchrsum2  27394  dchrhash  27397  sum2dchr  27400  lgsqrlem1  27472  lgsqrlem2  27473  lgsqrlem3  27474  lgsqrlem4  27475  lgsdchr  27481  lgseisenlem3  27503  lgseisenlem4  27504  dchrisum0flblem1  27634  dchrisum0re  27639  unitprodclb  33642  ringlsmss1  33647  crngmxidl  33693  mxidlprm  33694  dflringlem3  33727  dflring3  33728  idlsrgmulrss1  33742  psrmonprod  33883  esplyfvaln  33905  mdetpmtr1  34154  mdetpmtr12  34156  madjusmdetlem1  34158  madjusmdetlem4  34161  mdetlap  34163  zarcls1  34200  zarclsint  34203  zarclssn  34204  zartopn  34206  zart0  34210  zarcmplem  34212  rspectps  34214  aks6d1c1p2  42761  aks6d1c1p7  42765  aks6d1c1p6  42766  aks6d1c1  42768  hashscontpowcl  42772  hashscontpow  42774  aks6d1c4  42776  aks6d1c2lem3  42778  aks6d1c2  42782  aks6d1c5lem1  42788  aks6d1c5lem3  42789  aks6d1c6lem1  42822  aks6d1c6lem3  42824  aks6d1c6lem5  42829  aks6d1c7lem1  42832  aks5lem1  42838  aks5lem2  42839  aks5lem5a  42843  frlmpwfi  43710  isnumbasgrplem3  43717  mendlmod  43801  idomodle  43803  2zrng0  48891  cznabel  48907  cznrng  48908  crhmsubcALTV  48974  fldcatALTV  48978  fldhmsubcALTV  48980  crngprmringidom  48988  mgpsumz  49020  mgpsumn  49021  evl1at0  49049  evl1at1  49050