Theorem ringmnd 20190

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 20185	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2	1	grpmndd 18888	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18671  Ringcrg 20180

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-grp 18878  df-ring 20182

This theorem is referenced by:  ringmgm  20191  gsummulc1OLD  20261  gsummulc2OLD  20262  gsummulc1  20263  gsummulc2  20264  gsummgp0  20265  prdsringd  20268  pwsco1rhm  20447  suborng  20821  lmodvsmmulgdi  20860  rngqiprngimf1  21267  cnfldmulg  21370  cnsubmlem  21381  gsumfsum  21401  nn0srg  21404  rge0srg  21405  zring0  21425  freshmansdream  21541  re0g  21579  uvcresum  21760  psrlidm  21929  psrridm  21930  mplsubrglem  21971  mplmonmul  22003  evlslem2  22046  evlslem3  22047  evlsgsumadd  22063  mhpmulcl  22104  coe1tmmul2  22230  coe1tmmul  22231  cply1mul  22252  gsummoncoe1  22264  evls1gsumadd  22280  mamudi  22359  mamudir  22360  mamulid  22397  mamurid  22398  mat1dimmul  22432  mat1mhm  22440  dmatmul  22453  scmatscm  22469  1mavmul  22504  mulmarep1gsum1  22529  mdet0pr  22548  m1detdiag  22553  mdetdiag  22555  mdet0  22562  m2detleib  22587  maducoeval2  22596  madugsum  22599  smadiadetlem1a  22619  smadiadetlem3  22624  smadiadet  22626  cpmatmcllem  22674  mat2pmatghm  22686  mat2pmatmul  22687  pmatcollpw3fi1lem1  22742  idpm2idmp  22757  mp2pm2mplem4  22765  pm2mpghm  22772  monmat2matmon  22780  pm2mp  22781  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  cpmadugsumlemF  22832  cayhamlem4  22844  tdeglem4  26033  tdeglem2  26034  mdegmullem  26051  coe1mul3  26072  plypf1  26185  tayl0  26337  jensen  26967  amgmlem  26968  elrgspnlem1  33335  elrgspnlem3  33337  subrdom  33378  xrge0slmod  33440  ressply1invg  33661  psrmonmul  33726  esplyfval1  33749  drgext0gsca  33768  ply1degltdimlem  33799  fedgmullem2  33807  extdg1id  33843  evls1fldgencl  33847  zringnm  34135  rezh  34146  ringexp0nn  42501  aks6d1c6lem1  42537  amgm2d  44551  amgm3d  44552  amgm4d  44553  2zrng0  48601  cznrng  48618  mgpsumz  48719  ply1mulgsumlem2  48744  amgmwlem  50158  amgmw2d  50160