MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  crngrng Structured version   Unicode version

Theorem crngrng 16641
Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
crngrng  |-  ( R  e.  CRing  ->  R  e.  Ring )

Proof of Theorem crngrng
StepHypRef Expression
1 eqid 2437 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21iscrng 16638 . 2  |-  ( R  e.  CRing 
<->  ( R  e.  Ring  /\  (mulGrp `  R )  e. CMnd ) )
32simplbi 460 1  |-  ( R  e.  CRing  ->  R  e.  Ring )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   ` cfv 5411  CMndccmn 16266  mulGrpcmgp 16577   Ringcrg 16631   CRingccrg 16632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rex 2715  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-iota 5374  df-fv 5419  df-cring 16634
This theorem is referenced by:  gsummgp0  16685  prdscrngd  16691  crngbinom  16699  dvdsunit  16741  unitmulclb  16743  unitabl  16746  idsrngd  16923  divscrng  17296  sraassa  17370  rlmassa  17371  asclrhm  17386  psrcrng  17459  psrassa  17460  mplcrng  17506  mplassa  17507  mplcoe2  17521  mplcoe2OLD  17522  mplbas2  17523  mplbas2OLD  17524  mplmon2mul  17555  mplind  17556  evlslem2  17569  evlslem6  17570  evlslem6OLD  17571  evlslem3  17572  evlslem1  17573  evlseu  17574  evlsval2  17578  evlrhm  17583  evlsscasrng  17584  evlsca  17585  evlsvarsrng  17586  evlvar  17587  mpfind  17594  ply1crng  17626  ply1assa  17627  ply1coe  17716  evls1rhmlem  17725  evls1gsumadd  17728  evls1gsummul  17729  evl1val  17732  evl1sca  17737  evl1scad  17738  evl1var  17739  evl1vard  17740  evls1var  17741  evls1scasrng  17742  evls1varsrng  17743  evl1subd  17745  evl1expd  17748  pf1const  17749  pf1id  17750  pf1ind  17758  evl1gsumdlem  17759  evl1gsumd  17760  evl1gsumadd  17761  evl1gsummul  17763  evl1varpw  17764  evl1scvarpw  17766  evl1scvarpwval  17767  evl1gsummon  17768  cnrng  17807  zringrng  17855  zring0  17862  zrng0  17868  znzrh2  17947  zncyg  17950  zndvds0  17952  znf1o  17953  zzngim  17954  znfld  17962  znchr  17964  znunit  17965  znrrg  17967  cygznlem3  17971  re0g  18011  mamuvs2  18279  matassa  18300  madetsumid  18315  madetsmelbas  18318  madetsmelbas2  18319  mdetleib2  18368  mdetf  18375  mdet1  18377  mdetrlin  18378  mdetrsca  18379  mdetrsca2  18380  mdetr0  18381  mdetrlin2  18382  mdetralt  18383  mdetero  18385  mdetmul  18398  maducoeval2  18415  maduf  18416  madutpos  18417  madugsum  18418  madurid  18419  madulid  18420  marep01ma  18435  smadiadetlem0  18436  smadiadetlem1a  18438  smadiadetlem3lem2  18442  smadiadetlem3  18443  smadiadetlem4  18444  smadiadet  18445  smadiadetglem1  18446  smadiadetglem2  18447  smadiadetg  18448  matinv  18452  matunit  18453  slesolinv  18455  slesolinvbi  18456  slesolex  18457  cramerimplem1  18458  cramerimplem2  18459  cramerimplem3  18460  cramerimp  18461  cramer  18466  fta1glem1  21606  fta1g  21608  fta1blem  21609  dchrelbas3  22546  dchrelbasd  22547  dchrzrh1  22552  dchrzrhmul  22554  dchrmulcl  22557  dchrn0  22558  dchrfi  22563  dchrghm  22564  dchrabs  22568  dchrinv  22569  dchrptlem1  22572  dchrptlem2  22573  dchrptlem3  22574  dchrsum2  22576  dchrhash  22579  sum2dchr  22582  lgsqrlem1  22649  lgsqrlem2  22650  lgsqrlem3  22651  lgsqrlem4  22652  lgsdchr  22656  lgseisenlem3  22659  lgseisenlem4  22660  dchrisum0flblem1  22726  dchrisum0re  22731  rdivmuldivd  26206  subofld  26231  frlmpwfi  29396  isnumbasgrplem3  29404  mendlmod  29493  idomrootle  29503  idomodle  29504  mgpsumz  30695  mgpsumn  30696  assa2ass  30738  assamulgscmlem2  30740  evl1at0  30751  evl1at1  30752  lply1binom  30754  lply1binomsc  30755  mat1dimcrng  30774  dmatcrng  30782  scmatcrng  30789  mdet0  30792  m1detdiag  30793  mdetdiaglem  30794  mdetdiag  30795
  Copyright terms: Public domain W3C validator