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

Theorem ringmnd 18496
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 18492 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 grpmnd 17369 . 2 (𝑅 ∈ Grp → 𝑅 ∈ Mnd)
31, 2syl 17 1 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Mndcmnd 17234  Grpcgrp 17362  Ringcrg 18487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-grp 17365  df-ring 18489
This theorem is referenced by:  ringmgm  18497  gsummulc1  18546  gsummulc2  18547  gsummgp0  18548  prdsringd  18552  pwsco1rhm  18678  lmodvsmmulgdi  18838  psrlidm  19343  psrridm  19344  mplsubrglem  19379  mplmonmul  19404  evlslem2  19452  evlslem3  19454  coe1tmmul2  19586  coe1tmmul  19587  cply1mul  19604  gsummoncoe1  19614  evls1gsumadd  19629  cnfldmulg  19718  cnsubmlem  19734  gsumfsum  19753  nn0srg  19756  rge0srg  19757  zring0  19768  re0g  19898  uvcresum  20072  mamudi  20149  mamudir  20150  mamulid  20187  mamurid  20188  mat1dimmul  20222  mat1mhm  20230  dmatmul  20243  scmatscm  20259  1mavmul  20294  mulmarep1gsum1  20319  mdet0pr  20338  m1detdiag  20343  mdetdiag  20345  mdet0  20352  m2detleib  20377  maducoeval2  20386  madugsum  20389  smadiadetlem1a  20409  smadiadetlem3  20414  smadiadet  20416  cpmatmcllem  20463  mat2pmatghm  20475  mat2pmatmul  20476  pmatcollpw3fi1lem1  20531  idpm2idmp  20546  mp2pm2mplem4  20554  pm2mpghm  20561  monmat2matmon  20569  pm2mp  20570  chfacfscmulgsum  20605  chfacfpmmulgsum  20609  cpmadugsumlemF  20621  cayhamlem4  20633  tdeglem4  23758  tdeglem2  23759  mdegmullem  23776  coe1mul3  23797  plypf1  23906  tayl0  24054  jensen  24649  amgmlem  24650  suborng  29642  xrge0slmod  29671  zringnm  29828  rezh  29839  amgm2d  38022  amgm3d  38023  amgm4d  38024  2zrng0  41256  cznrng  41273  mgpsumz  41459  ply1mulgsumlem2  41493  amgmwlem  41881  amgmw2d  41883
  Copyright terms: Public domain W3C validator