MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringcmn Structured version   Visualization version   GIF version

Theorem ringcmn 19631
Description: A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
ringcmn (𝑅 ∈ Ring → 𝑅 ∈ CMnd)

Proof of Theorem ringcmn
StepHypRef Expression
1 ringabl 19630 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Abel)
2 ablcmn 19209 . 2 (𝑅 ∈ Abel → 𝑅 ∈ CMnd)
31, 2syl 17 1 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  CMndccmn 19202  Abelcabl 19203  Ringcrg 19594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-nn 11860  df-2 11922  df-sets 16749  df-slot 16767  df-ndx 16777  df-base 16793  df-plusg 16847  df-0g 16978  df-mgm 18146  df-sgrp 18195  df-mnd 18206  df-grp 18400  df-minusg 18401  df-cmn 19204  df-abl 19205  df-mgp 19537  df-ur 19549  df-ring 19596
This theorem is referenced by:  ringsrg  19639  gsummulc1  19656  gsummulc2  19657  gsumdixp  19659  gsumfsum  20462  nn0srg  20465  rge0srg  20466  regsumsupp  20616  ip2di  20635  frlmphl  20775  psrmulcllem  20943  psrlidm  20959  psrridm  20960  psrass1  20961  psrdi  20962  psrdir  20963  psrcom  20965  mplmonmul  21024  mplcoe1  21025  evlslem2  21070  evlslem1  21073  evlsgsumadd  21082  mhpmulcl  21120  psropprmul  21190  coe1mul2  21221  coe1fzgsumdlem  21253  gsumsmonply1  21255  gsummoncoe1  21256  lply1binom  21258  evls1gsumadd  21271  evl1gsumdlem  21303  mamucl  21329  mamuass  21330  mamudi  21331  mamudir  21332  mat1dimmul  21404  dmatmul  21425  mavmulcl  21475  mavmulass  21477  mdetleib2  21516  mdetf  21523  mdetrlin  21530  mdetralt  21536  m2detleib  21559  madugsum  21571  smadiadetlem3lem2  21595  smadiadet  21598  mat2pmatmul  21659  m2pmfzgsumcl  21676  decpmatmul  21700  pmatcollpw1  21704  pmatcollpwfi  21710  pmatcollpw3fi1lem1  21714  pm2mpcl  21725  mply1topmatcl  21733  mp2pm2mplem2  21735  mp2pm2mplem4  21737  mp2pm2mp  21739  pm2mpghm  21744  pm2mpmhmlem2  21747  pm2mp  21753  chfacfscmulgsum  21788  chfacfpmmulgsum  21792  cpmadugsumlemF  21804  cpmadugsumfi  21805  cayhamlem4  21816  tdeglem1  24984  tdeglem1OLD  24985  tdeglem3  24986  tdeglem3OLD  24987  tdeglem4  24988  tdeglem4OLD  24989  plypf1  25137  taylfvallem  25281  taylf  25284  tayl0  25285  taylpfval  25288  jensenlem1  25900  jensenlem2  25901  jensen  25902  amgm  25904  freshmansdream  31234  ofldchr  31263  elrspunidl  31351  fedgmullem1  31455  fedgmullem2  31456  mdetpmtr1  31518  zarcmplem  31576  matunitlindflem1  35546  lfladdcl  36858  mhphflem  40042  ply1mulgsum  45449  amgmwlem  46222
  Copyright terms: Public domain W3C validator