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

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

Proof of Theorem rngmnd
StepHypRef Expression
1 rnggrp 16638 . 2  |-  ( R  e.  Ring  ->  R  e. 
Grp )
2 grpmnd 15541 . 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 1756   Mndcmnd 15401   Grpcgrp 15402   Ringcrg 16633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-grp 15536  df-rng 16635
This theorem is referenced by:  gsummulc1  16683  gsummulc2  16684  gsummulc1OLD  16685  gsummulc2OLD  16686  gsummgp0  16687  prdsrngd  16692  pwsco1rhm  16808  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  mplsubrglem  17494  mplsubrglemOLD  17495  mplmonmul  17520  evlslem2  17572  evlslem3  17575  coe1tmmul2  17704  coe1tmmul  17705  evls1gsumadd  17734  cnfldmulg  17823  cnsubmlem  17836  gsumfsum  17854  nn0srg  17856  rge0srg  17857  zring0  17868  zrng0  17874  re0g  18017  uvcresum  18193  mamulid  18279  mamurid  18280  mamudi  18282  mamudir  18283  1mavmul  18334  mulmarep1gsum1  18359  mdet0pr  18378  mdet1  18383  m2detleib  18412  maducoeval2  18421  madugsum  18424  smadiadetlem1a  18444  smadiadetlem3  18449  smadiadet  18451  tdeglem4  21504  tdeglem2  21505  mdegmullem  21524  coe1mul3  21546  plypf1  21655  tayl0  21802  jensen  22357  amgmlem  22358  suborng  26234  xrge0slmod  26264  zringnm  26340  zzsnmOLD  26342  cnzh  26351  rezh  26352  mgpsumz  30711  lmodvsmmulgdi  30752  mat1dimmul  30795  dmatmul  30799  mdet0  30822  m1detdiag  30823  mdetdiag  30825
  Copyright terms: Public domain W3C validator