Theorem crngring 20203

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6530  CMndccmn 19759  mulGrpcmgp 20098  Ringcrg 20191  CRingccrg 20192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-cring 20194

This theorem is referenced by:  crngringd  20204  gsummgp0  20276  prdscrngd  20280  crngbinom  20293  dvdsunit  20337  unitmulclb  20339  unitabl  20342  rdivmuldivd  20371  crhmsubc  20640  fldcat  20741  fldhmsubc  20743  idsrngd  20814  rmodislmod  20885  quscrng  21242  cnring  21351  zringring  21408  zring0  21417  znzrh2  21504  zncyg  21507  zndvds0  21509  znf1o  21510  zzngim  21511  znfld  21519  znchr  21521  znunit  21522  znrrg  21524  cygznlem3  21528  freshmansdream  21533  re0g  21570  sraassa  21827  sraassaOLD  21828  rlmassa  21829  psrcrng  21930  mplcrng  21979  mplassa  21980  mplcoe2  21997  mplbas2  21998  mplmon2mul  22025  mplind  22026  evlslem2  22035  evlslem3  22036  evlslem6  22037  evlseu  22039  evlsval2  22043  evlsgsumadd  22047  evlsgsummul  22048  evlrhm  22052  evlsscasrng  22053  evlsca  22054  evlsvarsrng  22055  evlvar  22056  mpfind  22063  ply1crng  22132  ply1assa  22133  ply1chr  22242  lply1binom  22246  lply1binomsc  22247  evls1rhmlem  22257  evls1gsumadd  22260  evls1gsummul  22261  evl1val  22265  evl1sca  22270  evl1scad  22271  evl1var  22272  evl1vard  22273  evls1var  22274  evls1scasrng  22275  evls1varsrng  22276  evl1subd  22278  evl1expd  22281  pf1const  22282  pf1id  22283  pf1ind  22291  evl1gsumdlem  22292  evl1gsumd  22293  evl1gsumadd  22294  evl1gsummul  22296  evl1varpw  22297  evl1scvarpw  22299  evl1scvarpwval  22300  evl1gsummon  22301  evls1vsca  22309  mamuvs2  22342  matassa  22380  madetsumid  22397  madetsmelbas  22400  madetsmelbas2  22401  mat1dimcrng  22413  dmatcrng  22438  scmatcrng  22457  mdetleib2  22524  mdetf  22531  m1detdiag  22533  mdetdiaglem  22534  mdetdiag  22535  mdet1  22537  mdetrlin  22538  mdetrsca2  22540  mdetr0  22541  mdet0  22542  mdetrlin2  22543  mdetralt  22544  mdetero  22546  mdetmul  22559  maducoeval2  22576  maduf  22577  madutpos  22578  madugsum  22579  madurid  22580  madulid  22581  marep01ma  22596  smadiadetlem0  22597  smadiadetlem1a  22599  smadiadetlem3lem2  22603  smadiadetlem3  22604  smadiadetlem4  22605  smadiadet  22606  smadiadetglem1  22607  smadiadetglem2  22608  smadiadetg  22609  matinv  22613  matunit  22614  slesolinv  22616  slesolinvbi  22617  slesolex  22618  cramerimplem1  22619  cramerimplem2  22620  cramerimplem3  22621  cramerimp  22622  cramer  22627  mat2pmatmul  22667  mat2pmatmhm  22669  mat2pmatrhm  22670  mat2pmatlin  22671  m2cpmmhm  22681  m2cpmrhm  22682  m2pmfzgsumcl  22684  m2cpmrngiso  22694  monmatcollpw  22715  pmatcollpwlem  22716  pmatcollpw  22717  pmatcollpwfi  22718  pmatcollpw3fi1lem2  22723  pmatcollpwscmat  22727  monmat2matmon  22760  pm2mp  22761  chpmatply1  22768  chpmat1d  22772  chpdmat  22777  chpscmat  22778  chpscmatgsumbin  22780  chpscmatgsummon  22781  chp0mat  22782  chpidmat  22783  chmaidscmat  22784  chfacfscmulcl  22793  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmulcl  22797  chfacfpmmul0  22798  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadurid  22803  cpmidgsumm2pm  22805  cpmidpmatlem2  22807  cpmidpmatlem3  22808  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cpmadugsumfi  22813  cpmidgsum2  22815  cpmadumatpolylem1  22817  cpmadumatpolylem2  22818  cpmadumatpoly  22819  cayhamlem2  22820  chcoeffeqlem  22821  cayhamlem4  22824  cayleyhamilton0  22825  cayleyhamiltonALT  22827  cayleyhamilton1  22828  recvsOLD  25096  fta1glem1  26123  fta1g  26125  fta1blem  26126  idomrootle  26128  dchrelbas3  27199  dchrelbasd  27200  dchrzrh1  27205  dchrzrhmul  27207  dchrmulcl  27210  dchrn0  27211  dchrfi  27216  dchrghm  27217  dchrabs  27221  dchrinv  27222  dchrptlem1  27225  dchrptlem2  27226  dchrptlem3  27227  dchrsum2  27229  dchrhash  27232  sum2dchr  27235  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  lgsdchr  27316  lgseisenlem3  27338  lgseisenlem4  27339  dchrisum0flblem1  27469  dchrisum0re  27474  subofld  33284  unitprodclb  33350  ringlsmss1  33357  isprmidlc  33408  prmidl0  33411  qsidomlem1  33413  qsidomlem2  33414  crngmxidl  33430  mxidlprm  33431  idlsrgmulrss1  33472  mdetpmtr1  33800  mdetpmtr12  33802  madjusmdetlem1  33804  madjusmdetlem4  33807  mdetlap  33809  zarcls1  33846  zarclsint  33849  zarclssn  33850  zartopn  33852  zart0  33856  zarcmplem  33858  rspectps  33860  aks6d1c1p2  42068  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1  42075  hashscontpowcl  42079  hashscontpow  42081  aks6d1c4  42083  aks6d1c2lem3  42085  aks6d1c2  42089  aks6d1c5lem1  42095  aks6d1c5lem3  42096  aks6d1c6lem1  42129  aks6d1c6lem3  42131  aks6d1c6lem5  42136  aks6d1c7lem1  42139  aks5lem1  42145  aks5lem2  42146  aks5lem5a  42150  frlmpwfi  43069  isnumbasgrplem3  43076  mendlmod  43160  idomodle  43162  2zrng0  48167  cznabel  48183  cznrng  48184  crhmsubcALTV  48250  fldcatALTV  48254  fldhmsubcALTV  48256  mgpsumz  48285  mgpsumn  48286  evl1at0  48315  evl1at1  48316