Theorem crngring 20180

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6492  CMndccmn 19709  mulGrpcmgp 20075  Ringcrg 20168  CRingccrg 20169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-cring 20171

This theorem is referenced by:  crngringd  20181  gsummgp0  20253  prdscrngd  20257  crngbinom  20271  dvdsunit  20315  unitmulclb  20317  unitabl  20320  rdivmuldivd  20349  crhmsubc  20615  fldcat  20716  fldhmsubc  20718  idsrngd  20789  subofld  20810  rmodislmod  20881  quscrng  21238  cnring  21345  zringring  21404  zring0  21413  znzrh2  21500  zncyg  21503  zndvds0  21505  znf1o  21506  zzngim  21507  znfld  21515  znchr  21517  znunit  21518  znrrg  21520  cygznlem3  21524  freshmansdream  21529  re0g  21567  sraassa  21824  sraassaOLD  21825  rlmassa  21826  psrcrng  21927  mplcrng  21976  mplassa  21977  mplcoe2  21996  mplbas2  21997  mplmon2mul  22024  mplind  22025  evlslem2  22034  evlslem3  22035  evlslem6  22036  evlseu  22038  evlsval2  22042  evlsgsumadd  22051  evlsgsummul  22052  evlrhm  22056  evlsscasrng  22060  evlsca  22061  evlsvarsrng  22062  evlvar  22063  mpfind  22070  ply1crng  22139  ply1assa  22140  ply1chr  22250  lply1binom  22254  lply1binomsc  22255  evls1rhmlem  22265  evls1gsumadd  22268  evls1gsummul  22269  evl1val  22273  evl1sca  22278  evl1scad  22279  evl1var  22280  evl1vard  22281  evls1var  22282  evls1scasrng  22283  evls1varsrng  22284  evl1subd  22286  evl1expd  22289  pf1const  22290  pf1id  22291  pf1ind  22299  evl1gsumdlem  22300  evl1gsumd  22301  evl1gsumadd  22302  evl1gsummul  22304  evl1varpw  22305  evl1scvarpw  22307  evl1scvarpwval  22308  evl1gsummon  22309  evls1vsca  22317  mamuvs2  22350  matassa  22388  madetsumid  22405  madetsmelbas  22408  madetsmelbas2  22409  mat1dimcrng  22421  dmatcrng  22446  scmatcrng  22465  mdetleib2  22532  mdetf  22539  m1detdiag  22541  mdetdiaglem  22542  mdetdiag  22543  mdet1  22545  mdetrlin  22546  mdetrsca2  22548  mdetr0  22549  mdet0  22550  mdetrlin2  22551  mdetralt  22552  mdetero  22554  mdetmul  22567  maducoeval2  22584  maduf  22585  madutpos  22586  madugsum  22587  madurid  22588  madulid  22589  marep01ma  22604  smadiadetlem0  22605  smadiadetlem1a  22607  smadiadetlem3lem2  22611  smadiadetlem3  22612  smadiadetlem4  22613  smadiadet  22614  smadiadetglem1  22615  smadiadetglem2  22616  smadiadetg  22617  matinv  22621  matunit  22622  slesolinv  22624  slesolinvbi  22625  slesolex  22626  cramerimplem1  22627  cramerimplem2  22628  cramerimplem3  22629  cramerimp  22630  cramer  22635  mat2pmatmul  22675  mat2pmatmhm  22677  mat2pmatrhm  22678  mat2pmatlin  22679  m2cpmmhm  22689  m2cpmrhm  22690  m2pmfzgsumcl  22692  m2cpmrngiso  22702  monmatcollpw  22723  pmatcollpwlem  22724  pmatcollpw  22725  pmatcollpwfi  22726  pmatcollpw3fi1lem2  22731  pmatcollpwscmat  22735  monmat2matmon  22768  pm2mp  22769  chpmatply1  22776  chpmat1d  22780  chpdmat  22785  chpscmat  22786  chpscmatgsumbin  22788  chpscmatgsummon  22789  chp0mat  22790  chpidmat  22791  chmaidscmat  22792  chfacfscmulcl  22801  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmulcl  22805  chfacfpmmul0  22806  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadurid  22811  cpmidgsumm2pm  22813  cpmidpmatlem2  22815  cpmidpmatlem3  22816  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cpmadugsumfi  22821  cpmidgsum2  22823  cpmadumatpolylem1  22825  cpmadumatpolylem2  22826  cpmadumatpoly  22827  cayhamlem2  22828  chcoeffeqlem  22829  cayhamlem4  22832  cayleyhamilton0  22833  cayleyhamiltonALT  22835  cayleyhamilton1  22836  fta1glem1  26129  fta1g  26131  fta1blem  26132  idomrootle  26134  dchrelbas3  27205  dchrelbasd  27206  dchrzrh1  27211  dchrzrhmul  27213  dchrmulcl  27216  dchrn0  27217  dchrfi  27222  dchrghm  27223  dchrabs  27227  dchrinv  27228  dchrptlem1  27231  dchrptlem2  27232  dchrptlem3  27233  dchrsum2  27235  dchrhash  27238  sum2dchr  27241  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  lgsdchr  27322  lgseisenlem3  27344  lgseisenlem4  27345  dchrisum0flblem1  27475  dchrisum0re  27480  unitprodclb  33470  ringlsmss1  33477  isprmidlc  33528  prmidl0  33531  qsidomlem1  33533  qsidomlem2  33534  crngmxidl  33550  mxidlprm  33551  idlsrgmulrss1  33592  mdetpmtr1  33980  mdetpmtr12  33982  madjusmdetlem1  33984  madjusmdetlem4  33987  mdetlap  33989  zarcls1  34026  zarclsint  34029  zarclssn  34030  zartopn  34032  zart0  34036  zarcmplem  34038  rspectps  34040  aks6d1c1p2  42363  aks6d1c1p7  42367  aks6d1c1p6  42368  aks6d1c1  42370  hashscontpowcl  42374  hashscontpow  42376  aks6d1c4  42378  aks6d1c2lem3  42380  aks6d1c2  42384  aks6d1c5lem1  42390  aks6d1c5lem3  42391  aks6d1c6lem1  42424  aks6d1c6lem3  42426  aks6d1c6lem5  42431  aks6d1c7lem1  42434  aks5lem1  42440  aks5lem2  42441  aks5lem5a  42445  frlmpwfi  43340  isnumbasgrplem3  43347  mendlmod  43431  idomodle  43433  2zrng0  48490  cznabel  48506  cznrng  48507  crhmsubcALTV  48573  fldcatALTV  48577  fldhmsubcALTV  48579  mgpsumz  48608  mgpsumn  48609  evl1at0  48637  evl1at1  48638