Theorem crngring 20328

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

Syntax hints:   → wi 4   ∈ wcel 2143  ‘cfv 6538  CMndccmn 19851  mulGrpcmgp 20217  Ringcrg 20316  CRingccrg 20317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-cring 20319

This theorem is referenced by:  crngringd  20329  gsummgp0  20400  prdscrngd  20404  crngbinom  20418  dvdsunit  20462  unitmulclb  20464  unitabl  20467  rdivmuldivd  20496  crhmsubc  20768  fldcat  20867  fldhmsubc  20869  idsrngd  20940  subofld  20961  rmodislmod  21032  isfieldidl  21367  isfieldidl2  21368  df2idl2crng  21402  quscrng  21404  isprmidlc  21453  cmprmidlmcl  21456  prmidl0  21459  qsidomlem1  21461  qsidomlem2  21462  prmidlsubm  21468  cnring  21525  zringring  21580  zring0  21589  znzrh2  21676  zncyg  21679  zndvds0  21681  znf1o  21682  zzngim  21683  znfld  21691  znchr  21693  znunit  21694  znrrg  21696  cygznlem3  21700  freshmansdream  21705  re0g  21743  sraassa  22000  rlmassa  22001  psrcrng  22102  mplcrng  22151  mplassa  22152  mplcoe2  22173  mplbas2  22174  mplmon2mul  22201  mplind  22202  evlslem2  22211  evlslem3  22212  evlslem6  22213  evlseu  22215  evlsval2  22219  evlsgsumadd  22228  evlsgsummul  22229  evlrhm  22233  evlsscasrng  22237  evlsca  22238  evlsvarsrng  22239  evlvar  22240  mpfind  22247  ply1crng  22339  ply1assa  22340  ply1chr  22447  lply1binom  22451  lply1binomsc  22452  evls1rhmlem  22462  evls1gsumadd  22465  evls1gsummul  22466  evl1val  22470  evl1sca  22475  evl1scad  22476  evl1var  22477  evl1vard  22478  evls1var  22479  evls1scasrng  22480  evls1varsrng  22481  evl1subd  22483  evl1expd  22486  pf1const  22487  pf1id  22488  pf1ind  22496  evl1gsumdlem  22497  evl1gsumd  22498  evl1gsumadd  22499  evl1gsummul  22501  evl1varpw  22502  evl1scvarpw  22504  evl1scvarpwval  22505  evl1gsummon  22506  evls1vsca  22514  mamuvs2  22544  matassa  22582  madetsumid  22599  madetsmelbas  22602  madetsmelbas2  22603  mat1dimcrng  22615  dmatcrng  22640  scmatcrng  22659  mdetleib2  22726  mdetf  22733  m1detdiag  22735  mdetdiaglem  22736  mdetdiag  22737  mdet1  22739  mdetrlin  22740  mdetrsca2  22742  mdetr0  22743  mdet0  22744  mdetrlin2  22745  mdetralt  22746  mdetero  22748  mdetmul  22761  maducoeval2  22778  maduf  22779  madutpos  22780  madugsum  22781  madurid  22782  madulid  22783  marep01ma  22798  smadiadetlem0  22799  smadiadetlem1a  22801  smadiadetlem3lem2  22805  smadiadetlem3  22806  smadiadetlem4  22807  smadiadet  22808  smadiadetglem1  22809  smadiadetglem2  22810  smadiadetg  22811  matinv  22815  matunit  22816  slesolinv  22818  slesolinvbi  22819  slesolex  22820  cramerimplem1  22821  cramerimplem2  22822  cramerimplem3  22823  cramerimp  22824  cramer  22829  mat2pmatmul  22869  mat2pmatmhm  22871  mat2pmatrhm  22872  mat2pmatlin  22873  m2cpmmhm  22883  m2cpmrhm  22884  m2pmfzgsumcl  22886  m2cpmrngiso  22896  monmatcollpw  22917  pmatcollpwlem  22918  pmatcollpw  22919  pmatcollpwfi  22920  pmatcollpw3fi1lem2  22925  pmatcollpwscmat  22929  monmat2matmon  22962  pm2mp  22963  chpmatply1  22970  chpmat1d  22974  chpdmat  22979  chpscmat  22980  chpscmatgsumbin  22982  chpscmatgsummon  22983  chp0mat  22984  chpidmat  22985  chmaidscmat  22986  chfacfscmulcl  22995  chfacfscmul0  22996  chfacfscmulgsum  22998  chfacfpmmulcl  22999  chfacfpmmul0  23000  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadurid  23005  cpmidgsumm2pm  23007  cpmidpmatlem2  23009  cpmidpmatlem3  23010  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cpmadugsumfi  23015  cpmidgsum2  23017  cpmadumatpolylem1  23019  cpmadumatpolylem2  23020  cpmadumatpoly  23021  cayhamlem2  23022  chcoeffeqlem  23023  cayhamlem4  23026  cayleyhamilton0  23027  cayleyhamiltonALT  23029  cayleyhamilton1  23030  fta1glem1  26306  fta1g  26308  fta1blem  26309  idomrootle  26311  dchrelbas3  27383  dchrelbasd  27384  dchrzrh1  27389  dchrzrhmul  27391  dchrmulcl  27394  dchrn0  27395  dchrfi  27400  dchrghm  27401  dchrabs  27405  dchrinv  27406  dchrptlem1  27409  dchrptlem2  27410  dchrptlem3  27411  dchrsum2  27413  dchrhash  27416  sum2dchr  27419  lgsqrlem1  27491  lgsqrlem2  27492  lgsqrlem3  27493  lgsqrlem4  27494  lgsdchr  27500  lgseisenlem3  27522  lgseisenlem4  27523  dchrisum0flblem1  27653  dchrisum0re  27658  unitprodclb  33683  ringlsmss1  33688  crngmxidl  33733  mxidlprm  33734  dflringlem3  33767  dflring3  33768  idlsrgmulrss1  33782  psrmonprod  33923  esplyfvaln  33945  mdetpmtr1  34194  mdetpmtr12  34196  madjusmdetlem1  34198  madjusmdetlem4  34201  mdetlap  34203  zarcls1  34240  zarclsint  34243  zarclssn  34244  zartopn  34246  zart0  34250  zarcmplem  34252  rspectps  34254  aks6d1c1p2  42857  aks6d1c1p7  42861  aks6d1c1p6  42862  aks6d1c1  42864  hashscontpowcl  42868  hashscontpow  42870  aks6d1c4  42872  aks6d1c2lem3  42874  aks6d1c2  42878  aks6d1c5lem1  42884  aks6d1c5lem3  42885  aks6d1c6lem1  42918  aks6d1c6lem3  42920  aks6d1c6lem5  42925  aks6d1c7lem1  42928  aks5lem1  42934  aks5lem2  42935  aks5lem5a  42939  frlmpwfi  43808  isnumbasgrplem3  43815  mendlmod  43899  idomodle  43901  2zrng0  48992  cznabel  49008  cznrng  49009  crhmsubcALTV  49075  fldcatALTV  49079  fldhmsubcALTV  49081  crngprmringidom  49089  isidom3  49093  idomcanl  49095  mgpsumz  49125  mgpsumn  49126  evl1at0  49154  evl1at1  49155