Theorem crngring 20272

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  CMndccmn 19822  mulGrpcmgp 20161  Ringcrg 20260  CRingccrg 20261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-cring 20263

This theorem is referenced by:  crngringd  20273  gsummgp0  20341  prdscrngd  20345  crngbinom  20358  dvdsunit  20405  unitmulclb  20407  unitabl  20410  rdivmuldivd  20439  crhmsubc  20704  fldcat  20806  fldhmsubc  20808  idsrngd  20879  rmodislmod  20950  rmodislmodOLD  20951  quscrng  21316  cnring  21426  zringring  21483  zring0  21492  znzrh2  21587  zncyg  21590  zndvds0  21592  znf1o  21593  zzngim  21594  znfld  21602  znchr  21604  znunit  21605  znrrg  21607  cygznlem3  21611  freshmansdream  21616  re0g  21653  sraassa  21912  sraassaOLD  21913  rlmassa  21914  psrcrng  22015  mplcrng  22064  mplassa  22065  mplcoe2  22082  mplbas2  22083  mplmon2mul  22116  mplind  22117  evlslem2  22126  evlslem3  22127  evlslem6  22128  evlseu  22130  evlsval2  22134  evlsgsumadd  22138  evlsgsummul  22139  evlrhm  22143  evlsscasrng  22144  evlsca  22145  evlsvarsrng  22146  evlvar  22147  mpfind  22154  ply1crng  22221  ply1assa  22222  ply1chr  22331  lply1binom  22335  lply1binomsc  22336  evls1rhmlem  22346  evls1gsumadd  22349  evls1gsummul  22350  evl1val  22354  evl1sca  22359  evl1scad  22360  evl1var  22361  evl1vard  22362  evls1var  22363  evls1scasrng  22364  evls1varsrng  22365  evl1subd  22367  evl1expd  22370  pf1const  22371  pf1id  22372  pf1ind  22380  evl1gsumdlem  22381  evl1gsumd  22382  evl1gsumadd  22383  evl1gsummul  22385  evl1varpw  22386  evl1scvarpw  22388  evl1scvarpwval  22389  evl1gsummon  22390  evls1vsca  22398  mamuvs2  22431  matassa  22471  madetsumid  22488  madetsmelbas  22491  madetsmelbas2  22492  mat1dimcrng  22504  dmatcrng  22529  scmatcrng  22548  mdetleib2  22615  mdetf  22622  m1detdiag  22624  mdetdiaglem  22625  mdetdiag  22626  mdet1  22628  mdetrlin  22629  mdetrsca2  22631  mdetr0  22632  mdet0  22633  mdetrlin2  22634  mdetralt  22635  mdetero  22637  mdetmul  22650  maducoeval2  22667  maduf  22668  madutpos  22669  madugsum  22670  madurid  22671  madulid  22672  marep01ma  22687  smadiadetlem0  22688  smadiadetlem1a  22690  smadiadetlem3lem2  22694  smadiadetlem3  22695  smadiadetlem4  22696  smadiadet  22697  smadiadetglem1  22698  smadiadetglem2  22699  smadiadetg  22700  matinv  22704  matunit  22705  slesolinv  22707  slesolinvbi  22708  slesolex  22709  cramerimplem1  22710  cramerimplem2  22711  cramerimplem3  22712  cramerimp  22713  cramer  22718  mat2pmatmul  22758  mat2pmatmhm  22760  mat2pmatrhm  22761  mat2pmatlin  22762  m2cpmmhm  22772  m2cpmrhm  22773  m2pmfzgsumcl  22775  m2cpmrngiso  22785  monmatcollpw  22806  pmatcollpwlem  22807  pmatcollpw  22808  pmatcollpwfi  22809  pmatcollpw3fi1lem2  22814  pmatcollpwscmat  22818  monmat2matmon  22851  pm2mp  22852  chpmatply1  22859  chpmat1d  22863  chpdmat  22868  chpscmat  22869  chpscmatgsumbin  22871  chpscmatgsummon  22872  chp0mat  22873  chpidmat  22874  chmaidscmat  22875  chfacfscmulcl  22884  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmulcl  22888  chfacfpmmul0  22889  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmadurid  22894  cpmidgsumm2pm  22896  cpmidpmatlem2  22898  cpmidpmatlem3  22899  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmidgsum2  22906  cpmadumatpolylem1  22908  cpmadumatpolylem2  22909  cpmadumatpoly  22910  cayhamlem2  22911  chcoeffeqlem  22912  cayhamlem4  22915  cayleyhamilton0  22916  cayleyhamiltonALT  22918  cayleyhamilton1  22919  recvsOLD  25199  fta1glem1  26227  fta1g  26229  fta1blem  26230  idomrootle  26232  dchrelbas3  27300  dchrelbasd  27301  dchrzrh1  27306  dchrzrhmul  27308  dchrmulcl  27311  dchrn0  27312  dchrfi  27317  dchrghm  27318  dchrabs  27322  dchrinv  27323  dchrptlem1  27326  dchrptlem2  27327  dchrptlem3  27328  dchrsum2  27330  dchrhash  27333  sum2dchr  27336  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem3  27410  lgsqrlem4  27411  lgsdchr  27417  lgseisenlem3  27439  lgseisenlem4  27440  dchrisum0flblem1  27570  dchrisum0re  27575  subofld  33311  unitprodclb  33382  ringlsmss1  33389  isprmidlc  33440  prmidl0  33443  qsidomlem1  33445  qsidomlem2  33446  crngmxidl  33462  mxidlprm  33463  idlsrgmulrss1  33504  mdetpmtr1  33769  mdetpmtr12  33771  madjusmdetlem1  33773  madjusmdetlem4  33776  mdetlap  33778  zarcls1  33815  zarclsint  33818  zarclssn  33819  zartopn  33821  zart0  33825  zarcmplem  33827  rspectps  33829  aks6d1c1p2  42066  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1  42073  hashscontpowcl  42077  hashscontpow  42079  aks6d1c4  42081  aks6d1c2lem3  42083  aks6d1c2  42087  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c6lem1  42127  aks6d1c6lem3  42129  aks6d1c6lem5  42134  aks6d1c7lem1  42137  aks5lem1  42143  aks5lem2  42144  aks5lem5a  42148  frlmpwfi  43055  isnumbasgrplem3  43062  mendlmod  43150  idomodle  43152  2zrng0  47967  cznabel  47983  cznrng  47984  crhmsubcALTV  48050  fldcatALTV  48054  fldhmsubcALTV  48056  mgpsumz  48087  mgpsumn  48088  evl1at0  48120  evl1at1  48121