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

Theorem ringmnd 17081
Description: A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
ringmnd  |-  ( R  e.  Ring  ->  R  e. 
Mnd )

Proof of Theorem ringmnd
StepHypRef Expression
1 ringgrp 17077 . 2  |-  ( R  e.  Ring  ->  R  e. 
Grp )
2 grpmnd 15936 . 2  |-  ( R  e.  Grp  ->  R  e.  Mnd )
31, 2syl 16 1  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   Mndcmnd 15793   Grpcgrp 15927   Ringcrg 17072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-nul 4566
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-grp 15931  df-ring 17074
This theorem is referenced by:  ringmgm  17082  gsummulc1  17126  gsummulc2  17127  gsummulc1OLD  17128  gsummulc2OLD  17129  gsummgp0  17130  prdsringd  17135  pwsco1rhm  17261  lmodvsmmulgdi  17421  psrlidm  17930  psrlidmOLD  17931  psrridm  17932  psrridmOLD  17933  mplsubrglem  17974  mplsubrglemOLD  17975  mplmonmul  18000  evlslem2  18054  evlslem3  18057  coe1tmmul2  18191  coe1tmmul  18192  cply1mul  18209  gsummoncoe1  18220  evls1gsumadd  18235  cnfldmulg  18324  cnsubmlem  18340  gsumfsum  18358  nn0srg  18360  rge0srg  18361  zring0  18372  zrng0  18378  re0g  18521  uvcresum  18697  mamudi  18778  mamudir  18779  mamulid  18816  mamurid  18817  mat1dimmul  18851  mat1mhm  18859  dmatmul  18872  scmatscm  18888  1mavmul  18923  mulmarep1gsum1  18948  mdet0pr  18967  m1detdiag  18972  mdetdiag  18974  mdet0  18981  m2detleib  19006  maducoeval2  19015  madugsum  19018  smadiadetlem1a  19038  smadiadetlem3  19043  smadiadet  19045  cpmatmcllem  19092  mat2pmatghm  19104  mat2pmatmul  19105  pmatcollpw3fi1lem1  19160  idpm2idmp  19175  mp2pm2mplem4  19183  pm2mpghm  19190  monmat2matmon  19198  pm2mp  19199  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  cpmadugsumlemF  19250  cayhamlem4  19262  tdeglem4  22331  tdeglem2  22332  mdegmullem  22351  coe1mul3  22373  plypf1  22482  tayl0  22629  jensen  23190  amgmlem  23191  suborng  27678  xrge0slmod  27707  zringnm  27813  zzsnmOLD  27815  rezh  27825  2zrng0  32454  cznrng  32473  mgpsumz  32685  ply1mulgsumlem2  32722
  Copyright terms: Public domain W3C validator