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

Theorem ringmnd 19303
Description: A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
ringmnd (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Proof of Theorem ringmnd
StepHypRef Expression
1 ringgrp 19298 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 grpmnd 18105 . 2 (𝑅 ∈ Grp → 𝑅 ∈ Mnd)
31, 2syl 17 1 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Mndcmnd 17906  Grpcgrp 18098  Ringcrg 19293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-grp 18101  df-ring 19295
This theorem is referenced by:  ringmgm  19304  gsummulc1  19355  gsummulc2  19356  gsummgp0  19357  prdsringd  19361  pwsco1rhm  19489  lmodvsmmulgdi  19665  cnfldmulg  20126  cnsubmlem  20142  gsumfsum  20161  nn0srg  20164  rge0srg  20165  zring0  20176  re0g  20304  uvcresum  20485  psrlidm  20644  psrridm  20645  mplsubrglem  20680  mplmonmul  20707  evlslem2  20754  evlslem3  20755  evlsgsumadd  20766  coe1tmmul2  20908  coe1tmmul  20909  cply1mul  20926  gsummoncoe1  20936  evls1gsumadd  20951  mamudi  21011  mamudir  21012  mamulid  21049  mamurid  21050  mat1dimmul  21084  mat1mhm  21092  dmatmul  21105  scmatscm  21121  1mavmul  21156  mulmarep1gsum1  21181  mdet0pr  21200  m1detdiag  21205  mdetdiag  21207  mdet0  21214  m2detleib  21239  maducoeval2  21248  madugsum  21251  smadiadetlem1a  21271  smadiadetlem3  21276  smadiadet  21278  cpmatmcllem  21326  mat2pmatghm  21338  mat2pmatmul  21339  pmatcollpw3fi1lem1  21394  idpm2idmp  21409  mp2pm2mplem4  21417  pm2mpghm  21424  monmat2matmon  21432  pm2mp  21433  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cpmadugsumlemF  21484  cayhamlem4  21496  tdeglem4  24664  tdeglem2  24665  mdegmullem  24682  coe1mul3  24703  plypf1  24812  tayl0  24960  jensen  25577  amgmlem  25578  freshmansdream  30912  suborng  30942  xrge0slmod  30971  drgext0gsca  31082  fedgmullem2  31114  extdg1id  31141  zringnm  31309  rezh  31320  amgm2d  40891  amgm3d  40892  amgm4d  40893  2zrng0  44549  cznrng  44566  mgpsumz  44751  ply1mulgsumlem2  44782  amgmwlem  45317  amgmw2d  45319
  Copyright terms: Public domain W3C validator