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

Theorem ringmnd 19235
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 19231 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 grpmnd 18048 . 2 (𝑅 ∈ Grp → 𝑅 ∈ Mnd)
31, 2syl 17 1 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Mndcmnd 17899  Grpcgrp 18041  Ringcrg 19226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-grp 18044  df-ring 19228
This theorem is referenced by:  ringmgm  19236  gsummulc1  19285  gsummulc2  19286  gsummgp0  19287  prdsringd  19291  pwsco1rhm  19419  lmodvsmmulgdi  19598  psrlidm  20111  psrridm  20112  mplsubrglem  20147  mplmonmul  20173  evlslem2  20220  evlslem3  20221  evlsgsumadd  20232  coe1tmmul2  20372  coe1tmmul  20373  cply1mul  20390  gsummoncoe1  20400  evls1gsumadd  20415  cnfldmulg  20505  cnsubmlem  20521  gsumfsum  20540  nn0srg  20543  rge0srg  20544  zring0  20555  re0g  20684  uvcresum  20865  mamudi  20940  mamudir  20941  mamulid  20978  mamurid  20979  mat1dimmul  21013  mat1mhm  21021  dmatmul  21034  scmatscm  21050  1mavmul  21085  mulmarep1gsum1  21110  mdet0pr  21129  m1detdiag  21134  mdetdiag  21136  mdet0  21143  m2detleib  21168  maducoeval2  21177  madugsum  21180  smadiadetlem1a  21200  smadiadetlem3  21205  smadiadet  21207  cpmatmcllem  21254  mat2pmatghm  21266  mat2pmatmul  21267  pmatcollpw3fi1lem1  21322  idpm2idmp  21337  mp2pm2mplem4  21345  pm2mpghm  21352  monmat2matmon  21360  pm2mp  21361  chfacfscmulgsum  21396  chfacfpmmulgsum  21400  cpmadugsumlemF  21412  cayhamlem4  21424  tdeglem4  24581  tdeglem2  24582  mdegmullem  24599  coe1mul3  24620  plypf1  24729  tayl0  24877  jensen  25493  amgmlem  25494  freshmansdream  30786  suborng  30815  xrge0slmod  30844  drgext0gsca  30893  fedgmullem2  30925  extdg1id  30952  zringnm  31100  rezh  31111  amgm2d  40429  amgm3d  40430  amgm4d  40431  2zrng0  44137  cznrng  44154  mgpsumz  44338  ply1mulgsumlem2  44369  amgmwlem  44831  amgmw2d  44833
  Copyright terms: Public domain W3C validator