Theorem ringmnd 20146

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

Step	Hyp	Ref	Expression
1		ringgrp 20141	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2	1	grpmndd 18843	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18626  Ringcrg 20136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-grp 18833  df-ring 20138

This theorem is referenced by:  ringmgm  20147  gsummulc1OLD  20217  gsummulc2OLD  20218  gsummulc1  20219  gsummulc2  20220  gsummgp0  20221  prdsringd  20224  pwsco1rhm  20405  suborng  20779  lmodvsmmulgdi  20818  rngqiprngimf1  21225  cnfldmulg  21328  cnsubmlem  21339  gsumfsum  21359  nn0srg  21362  rge0srg  21363  zring0  21383  freshmansdream  21499  re0g  21537  uvcresum  21718  psrlidm  21887  psrridm  21888  mplsubrglem  21929  mplmonmul  21959  evlslem2  22002  evlslem3  22003  evlsgsumadd  22014  mhpmulcl  22052  coe1tmmul2  22178  coe1tmmul  22179  cply1mul  22199  gsummoncoe1  22211  evls1gsumadd  22227  mamudi  22306  mamudir  22307  mamulid  22344  mamurid  22345  mat1dimmul  22379  mat1mhm  22387  dmatmul  22400  scmatscm  22416  1mavmul  22451  mulmarep1gsum1  22476  mdet0pr  22495  m1detdiag  22500  mdetdiag  22502  mdet0  22509  m2detleib  22534  maducoeval2  22543  madugsum  22546  smadiadetlem1a  22566  smadiadetlem3  22571  smadiadet  22573  cpmatmcllem  22621  mat2pmatghm  22633  mat2pmatmul  22634  pmatcollpw3fi1lem1  22689  idpm2idmp  22704  mp2pm2mplem4  22712  pm2mpghm  22719  monmat2matmon  22727  pm2mp  22728  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  cpmadugsumlemF  22779  cayhamlem4  22791  tdeglem4  25981  tdeglem2  25982  mdegmullem  25999  coe1mul3  26020  plypf1  26133  tayl0  26285  jensen  26915  amgmlem  26916  elrgspnlem1  33195  elrgspnlem3  33197  subrdom  33237  xrge0slmod  33298  ressply1invg  33517  drgext0gsca  33566  ply1degltdimlem  33597  fedgmullem2  33605  extdg1id  33640  evls1fldgencl  33644  zringnm  33927  rezh  33938  ringexp0nn  42110  aks6d1c6lem1  42146  amgm2d  44174  amgm3d  44175  amgm4d  44176  2zrng0  48232  cznrng  48249  mgpsumz  48350  ply1mulgsumlem2  48376  amgmwlem  49791  amgmw2d  49793