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

Theorem crngrng 16989
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 2460 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21iscrng 16986 . 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 1762   ` cfv 5579  CMndccmn 16587  mulGrpcmgp 16924   Ringcrg 16979   CRingccrg 16980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-cring 16982
This theorem is referenced by:  gsummgp0  17033  prdscrngd  17039  crngbinom  17047  dvdsunit  17089  unitmulclb  17091  unitabl  17094  idsrngd  17287  divscrng  17663  assa2ass  17735  sraassa  17738  rlmassa  17739  asclrhm  17755  assamulgscmlem2  17762  psrcrng  17832  psrassa  17833  mplcrng  17879  mplassa  17880  mplcoe2  17896  mplcoe2OLD  17897  mplbas2  17898  mplbas2OLD  17899  mplmon2mul  17930  mplind  17931  evlslem2  17944  evlslem6  17945  evlslem6OLD  17946  evlslem3  17947  evlslem1  17948  evlseu  17949  evlsval2  17953  evlrhm  17958  evlsscasrng  17959  evlsca  17960  evlsvarsrng  17961  evlvar  17962  mpfind  17969  ply1crng  18001  ply1assa  18002  ply1coeOLD  18102  lply1binom  18112  lply1binomsc  18113  evls1rhmlem  18122  evls1gsumadd  18125  evls1gsummul  18126  evl1val  18129  evl1sca  18134  evl1scad  18135  evl1var  18136  evl1vard  18137  evls1var  18138  evls1scasrng  18139  evls1varsrng  18140  evl1subd  18142  evl1expd  18145  pf1const  18146  pf1id  18147  pf1ind  18155  evl1gsumdlem  18156  evl1gsumd  18157  evl1gsumadd  18158  evl1gsummul  18160  evl1varpw  18161  evl1scvarpw  18163  evl1scvarpwval  18164  evl1gsummon  18165  cnrng  18204  zringrng  18252  zring0  18259  zrng0  18265  znzrh2  18344  zncyg  18347  zndvds0  18349  znf1o  18350  zzngim  18351  znfld  18359  znchr  18361  znunit  18362  znrrg  18364  cygznlem3  18368  re0g  18408  mamuvs2  18668  matassa  18706  madetsumid  18723  madetsmelbas  18726  madetsmelbas2  18727  mat1dimcrng  18739  dmatcrng  18764  scmatcrng  18783  mdetleib2  18850  mdetf  18857  m1detdiag  18859  mdetdiaglem  18860  mdetdiag  18861  mdet1  18863  mdetrlin  18864  mdetrsca  18865  mdetrsca2  18866  mdetr0  18867  mdet0  18868  mdetrlin2  18869  mdetralt  18870  mdetero  18872  mdetmul  18885  maducoeval2  18902  maduf  18903  madutpos  18904  madugsum  18905  madurid  18906  madulid  18907  marep01ma  18922  smadiadetlem0  18923  smadiadetlem1a  18925  smadiadetlem3lem2  18929  smadiadetlem3  18930  smadiadetlem4  18931  smadiadet  18932  smadiadetglem1  18933  smadiadetglem2  18934  smadiadetg  18935  matinv  18939  matunit  18940  slesolinv  18942  slesolinvbi  18943  slesolex  18944  cramerimplem1  18945  cramerimplem2  18946  cramerimplem3  18947  cramerimp  18948  cramer  18953  mat2pmatmul  18992  mat2pmatmhm  18994  mat2pmatrhm  18995  mat2pmatlin  18996  m2cpmmhm  19006  m2cpmrhm  19007  m2pmfzgsumcl  19009  m2cpmrngiso  19019  monmatcollpw  19040  pmatcollpwlem  19041  pmatcollpw  19042  pmatcollpwfi  19043  pmatcollpw3fi1lem2  19048  pmatcollpwscmat  19052  monmat2matmon  19085  pm2mp  19086  chpmatply1  19093  chpmat1d  19097  chpdmat  19102  chpscmat  19103  chpscmatgsumbin  19105  chpscmatgsummon  19106  chp0mat  19107  chpidmat  19108  chmaidscmat  19109  chfacfscmulcl  19118  chfacfscmul0  19119  chfacfscmulgsum  19121  chfacfpmmulcl  19122  chfacfpmmul0  19123  chfacfpmmulgsum  19125  chfacfpmmulgsum2  19126  cayhamlem1  19127  cpmadurid  19128  cpmidgsumm2pm  19130  cpmidpmatlem2  19132  cpmidpmatlem3  19133  cpmadugsumlemB  19135  cpmadugsumlemC  19136  cpmadugsumlemF  19137  cpmadugsumfi  19138  cpmidgsum2  19140  cpmadumatpolylem1  19142  cpmadumatpolylem2  19143  cpmadumatpoly  19144  cayhamlem2  19145  chcoeffeqlem  19146  cayhamlem4  19149  cayleyhamilton0  19150  cayleyhamiltonALT  19152  cayleyhamilton1  19153  fta1glem1  22294  fta1g  22296  fta1blem  22297  dchrelbas3  23234  dchrelbasd  23235  dchrzrh1  23240  dchrzrhmul  23242  dchrmulcl  23245  dchrn0  23246  dchrfi  23251  dchrghm  23252  dchrabs  23256  dchrinv  23257  dchrptlem1  23260  dchrptlem2  23261  dchrptlem3  23262  dchrsum2  23264  dchrhash  23267  sum2dchr  23270  lgsqrlem1  23337  lgsqrlem2  23338  lgsqrlem3  23339  lgsqrlem4  23340  lgsdchr  23344  lgseisenlem3  23347  lgseisenlem4  23348  dchrisum0flblem1  23414  dchrisum0re  23419  rdivmuldivd  27430  subofld  27455  frlmpwfi  30639  isnumbasgrplem3  30647  mendlmod  30736  idomrootle  30746  idomodle  30747  mgpsumz  31891  mgpsumn  31892  evl1at0  31939  evl1at1  31940
  Copyright terms: Public domain W3C validator