Theorem crngring 17407

Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
crngring	|- ( R e. CRing -> R e. Ring )

Proof of Theorem crngring

Step	Hyp	Ref	Expression
1		eqid 2454	. . 3 |- (mulGrp ` R ) = (mulGrp ` R )
2	1	iscrng 17403	. 2 |- ( R e. CRing <-> ( R e. Ring /\ (mulGrp ` R ) e. CMnd ) )
3	2	simplbi 458	1 |- ( R e. CRing -> R e. Ring )

Syntax hints:   -> wi 4   e. wcel 1823   ` cfv 5570  CMndccmn 17000  mulGrpcmgp 17339   Ringcrg 17396   CRingccrg 17397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-cring 17399

This theorem is referenced by:  gsummgp0  17454  prdscrngd  17460  crngbinom  17468  dvdsunit  17510  unitmulclb  17512  unitabl  17515  idsrngd  17709  quscrng  18086  assa2ass  18169  sraassa  18172  rlmassa  18173  asclrhm  18189  assamulgscmlem2  18196  psrcrng  18266  psrassa  18267  mplcrng  18313  mplassa  18314  mplcoe2  18330  mplcoe2OLD  18331  mplbas2  18332  mplbas2OLD  18333  mplmon2mul  18364  mplind  18365  evlslem2  18378  evlslem6  18379  evlslem6OLD  18380  evlslem3  18381  evlslem1  18382  evlseu  18383  evlsval2  18387  evlrhm  18392  evlsscasrng  18393  evlsca  18394  evlsvarsrng  18395  evlvar  18396  mpfind  18403  ply1crng  18435  ply1assa  18436  ply1coeOLD  18536  lply1binom  18546  lply1binomsc  18547  evls1rhmlem  18556  evls1gsumadd  18559  evls1gsummul  18560  evl1val  18563  evl1sca  18568  evl1scad  18569  evl1var  18570  evl1vard  18571  evls1var  18572  evls1scasrng  18573  evls1varsrng  18574  evl1subd  18576  evl1expd  18579  pf1const  18580  pf1id  18581  pf1ind  18589  evl1gsumdlem  18590  evl1gsumd  18591  evl1gsumadd  18592  evl1gsummul  18594  evl1varpw  18595  evl1scvarpw  18597  evl1scvarpwval  18598  evl1gsummon  18599  cnring  18638  zringring  18689  zring0  18696  znzrh2  18760  zncyg  18763  zndvds0  18765  znf1o  18766  zzngim  18767  znfld  18775  znchr  18777  znunit  18778  znrrg  18780  cygznlem3  18784  re0g  18824  mamuvs2  19078  matassa  19116  madetsumid  19133  madetsmelbas  19136  madetsmelbas2  19137  mat1dimcrng  19149  dmatcrng  19174  scmatcrng  19193  mdetleib2  19260  mdetf  19267  m1detdiag  19269  mdetdiaglem  19270  mdetdiag  19271  mdet1  19273  mdetrlin  19274  mdetrsca  19275  mdetrsca2  19276  mdetr0  19277  mdet0  19278  mdetrlin2  19279  mdetralt  19280  mdetero  19282  mdetmul  19295  maducoeval2  19312  maduf  19313  madutpos  19314  madugsum  19315  madurid  19316  madulid  19317  marep01ma  19332  smadiadetlem0  19333  smadiadetlem1a  19335  smadiadetlem3lem2  19339  smadiadetlem3  19340  smadiadetlem4  19341  smadiadet  19342  smadiadetglem1  19343  smadiadetglem2  19344  smadiadetg  19345  matinv  19349  matunit  19350  slesolinv  19352  slesolinvbi  19353  slesolex  19354  cramerimplem1  19355  cramerimplem2  19356  cramerimplem3  19357  cramerimp  19358  cramer  19363  mat2pmatmul  19402  mat2pmatmhm  19404  mat2pmatrhm  19405  mat2pmatlin  19406  m2cpmmhm  19416  m2cpmrhm  19417  m2pmfzgsumcl  19419  m2cpmrngiso  19429  monmatcollpw  19450  pmatcollpwlem  19451  pmatcollpw  19452  pmatcollpwfi  19453  pmatcollpw3fi1lem2  19458  pmatcollpwscmat  19462  monmat2matmon  19495  pm2mp  19496  chpmatply1  19503  chpmat1d  19507  chpdmat  19512  chpscmat  19513  chpscmatgsumbin  19515  chpscmatgsummon  19516  chp0mat  19517  chpidmat  19518  chmaidscmat  19519  chfacfscmulcl  19528  chfacfscmul0  19529  chfacfscmulgsum  19531  chfacfpmmulcl  19532  chfacfpmmul0  19533  chfacfpmmulgsum  19535  chfacfpmmulgsum2  19536  cayhamlem1  19537  cpmadurid  19538  cpmidgsumm2pm  19540  cpmidpmatlem2  19542  cpmidpmatlem3  19543  cpmadugsumlemB  19545  cpmadugsumlemC  19546  cpmadugsumlemF  19547  cpmadugsumfi  19548  cpmidgsum2  19550  cpmadumatpolylem1  19552  cpmadumatpolylem2  19553  cpmadumatpoly  19554  cayhamlem2  19555  chcoeffeqlem  19556  cayhamlem4  19559  cayleyhamilton0  19560  cayleyhamiltonALT  19562  cayleyhamilton1  19563  fta1glem1  22735  fta1g  22737  fta1blem  22738  dchrelbas3  23714  dchrelbasd  23715  dchrzrh1  23720  dchrzrhmul  23722  dchrmulcl  23725  dchrn0  23726  dchrfi  23731  dchrghm  23732  dchrabs  23736  dchrinv  23737  dchrptlem1  23740  dchrptlem2  23741  dchrptlem3  23742  dchrsum2  23744  dchrhash  23747  sum2dchr  23750  lgsqrlem1  23817  lgsqrlem2  23818  lgsqrlem3  23819  lgsqrlem4  23820  lgsdchr  23824  lgseisenlem3  23827  lgseisenlem4  23828  dchrisum0flblem1  23894  dchrisum0re  23899  rdivmuldivd  28019  subofld  28044  frlmpwfi  31290  isnumbasgrplem3  31298  mendlmod  31386  idomrootle  31396  idomodle  31397  2zrng0  33017  cznabel  33035  cznrng  33036  crhmsubc  33159  fldcat  33163  fldhmsubc  33165  crhmsubcALTV  33178  fldcatALTV  33182  fldhmsubcALTV  33184  mgpsumz  33225  mgpsumn  33226  evl1at0  33264  evl1at1  33265