Theorem ringmnd 20224

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18702  Ringcrg 20214

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 2708  ax-nul 5241

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-grp 18912  df-ring 20216

This theorem is referenced by:  ringmgm  20225  gsummulc1  20295  gsummulc2  20296  gsummgp0  20297  prdsringd  20300  pwsco1rhm  20479  suborng  20853  lmodvsmmulgdi  20892  rngqiprngimf1  21298  cnfldmulg  21384  cnsubmlem  21395  gsumfsum  21414  nn0srg  21417  rge0srg  21418  zring0  21438  freshmansdream  21554  re0g  21592  uvcresum  21773  psrlidm  21940  psrridm  21941  mplsubrglem  21982  mplmonmul  22014  evlslem2  22057  evlslem3  22058  evlsgsumadd  22074  mhpmulcl  22115  coe1tmmul2  22241  coe1tmmul  22242  cply1mul  22261  gsummoncoe1  22273  evls1gsumadd  22289  mamudi  22368  mamudir  22369  mamulid  22406  mamurid  22407  mat1dimmul  22441  mat1mhm  22449  dmatmul  22462  scmatscm  22478  1mavmul  22513  mulmarep1gsum1  22538  mdet0pr  22557  m1detdiag  22562  mdetdiag  22564  mdet0  22571  m2detleib  22596  maducoeval2  22605  madugsum  22608  smadiadetlem1a  22628  smadiadetlem3  22633  smadiadet  22635  cpmatmcllem  22683  mat2pmatghm  22695  mat2pmatmul  22696  pmatcollpw3fi1lem1  22751  idpm2idmp  22766  mp2pm2mplem4  22774  pm2mpghm  22781  monmat2matmon  22789  pm2mp  22790  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cpmadugsumlemF  22841  cayhamlem4  22853  tdeglem4  26025  tdeglem2  26026  mdegmullem  26043  coe1mul3  26064  plypf1  26177  tayl0  26327  jensen  26952  amgmlem  26953  elrgspnlem1  33303  elrgspnlem3  33305  subrdom  33346  xrge0slmod  33408  ressply1invg  33629  psrmonmul  33694  esplyfval1  33717  drgext0gsca  33736  ply1degltdimlem  33766  fedgmullem2  33774  extdg1id  33810  evls1fldgencl  33814  zringnm  34102  rezh  34113  ringexp0nn  42573  aks6d1c6lem1  42609  amgm2d  44625  amgm3d  44626  amgm4d  44627  2zrng0  48720  cznrng  48737  mgpsumz  48838  ply1mulgsumlem2  48863  amgmwlem  50277  amgmw2d  50279