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

Theorem crngrng 16658
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 2443 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21iscrng 16655 . 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 5421  CMndccmn 16280  mulGrpcmgp 16594   Ringcrg 16648   CRingccrg 16649
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 2423
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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-cring 16651
This theorem is referenced by:  gsummgp0  16702  prdscrngd  16708  crngbinom  16716  dvdsunit  16758  unitmulclb  16760  unitabl  16763  idsrngd  16950  divscrng  17325  sraassa  17399  rlmassa  17400  asclrhm  17415  psrcrng  17488  psrassa  17489  mplcrng  17535  mplassa  17536  mplcoe2  17552  mplcoe2OLD  17553  mplbas2  17554  mplbas2OLD  17555  mplmon2mul  17586  mplind  17587  evlslem2  17600  evlslem6  17601  evlslem6OLD  17602  evlslem3  17603  evlslem1  17604  evlseu  17605  evlsval2  17609  evlrhm  17614  evlsscasrng  17615  evlsca  17616  evlsvarsrng  17617  evlvar  17618  mpfind  17625  ply1crng  17657  ply1assa  17658  ply1coeOLD  17750  evls1rhmlem  17759  evls1gsumadd  17762  evls1gsummul  17763  evl1val  17766  evl1sca  17771  evl1scad  17772  evl1var  17773  evl1vard  17774  evls1var  17775  evls1scasrng  17776  evls1varsrng  17777  evl1subd  17779  evl1expd  17782  pf1const  17783  pf1id  17784  pf1ind  17792  evl1gsumdlem  17793  evl1gsumd  17794  evl1gsumadd  17795  evl1gsummul  17797  evl1varpw  17798  evl1scvarpw  17800  evl1scvarpwval  17801  evl1gsummon  17802  cnrng  17841  zringrng  17889  zring0  17896  zrng0  17902  znzrh2  17981  zncyg  17984  zndvds0  17986  znf1o  17987  zzngim  17988  znfld  17996  znchr  17998  znunit  17999  znrrg  18001  cygznlem3  18005  re0g  18045  mamuvs2  18313  matassa  18334  madetsumid  18349  madetsmelbas  18352  madetsmelbas2  18353  mdetleib2  18402  mdetf  18409  mdet1  18411  mdetrlin  18412  mdetrsca  18413  mdetrsca2  18414  mdetr0  18415  mdetrlin2  18416  mdetralt  18417  mdetero  18419  mdetmul  18432  maducoeval2  18449  maduf  18450  madutpos  18451  madugsum  18452  madurid  18453  madulid  18454  marep01ma  18469  smadiadetlem0  18470  smadiadetlem1a  18472  smadiadetlem3lem2  18476  smadiadetlem3  18477  smadiadetlem4  18478  smadiadet  18479  smadiadetglem1  18480  smadiadetglem2  18481  smadiadetg  18482  matinv  18486  matunit  18487  slesolinv  18489  slesolinvbi  18490  slesolex  18491  cramerimplem1  18492  cramerimplem2  18493  cramerimplem3  18494  cramerimp  18495  cramer  18500  fta1glem1  21640  fta1g  21642  fta1blem  21643  dchrelbas3  22580  dchrelbasd  22581  dchrzrh1  22586  dchrzrhmul  22588  dchrmulcl  22591  dchrn0  22592  dchrfi  22597  dchrghm  22598  dchrabs  22602  dchrinv  22603  dchrptlem1  22606  dchrptlem2  22607  dchrptlem3  22608  dchrsum2  22610  dchrhash  22613  sum2dchr  22616  lgsqrlem1  22683  lgsqrlem2  22684  lgsqrlem3  22685  lgsqrlem4  22686  lgsdchr  22690  lgseisenlem3  22693  lgseisenlem4  22694  dchrisum0flblem1  22760  dchrisum0re  22765  rdivmuldivd  26262  subofld  26287  frlmpwfi  29456  isnumbasgrplem3  29464  mendlmod  29553  idomrootle  29563  idomodle  29564  mgpsumz  30763  mgpsumn  30764  assa2ass  30822  assamulgscmlem2  30824  evl1at0  30852  evl1at1  30853  lply1binom  30854  lply1binomsc  30855  mat1dimcrng  30876  dmatcrng  30884  scmatcrng  30891  mdet0  30936  m1detdiag  30937  mdetdiaglem  30938  mdetdiag  30939
  Copyright terms: Public domain W3C validator