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

Theorem ringmnd 17405
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 17401 . 2  |-  ( R  e.  Ring  ->  R  e. 
Grp )
2 grpmnd 16264 . 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 1823   Mndcmnd 16121   Grpcgrp 16255   Ringcrg 17396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-grp 16259  df-ring 17398
This theorem is referenced by:  ringmgm  17406  gsummulc1  17450  gsummulc2  17451  gsummulc1OLD  17452  gsummulc2OLD  17453  gsummgp0  17454  prdsringd  17459  pwsco1rhm  17585  lmodvsmmulgdi  17745  psrlidm  18254  psrlidmOLD  18255  psrridm  18256  psrridmOLD  18257  mplsubrglem  18298  mplsubrglemOLD  18299  mplmonmul  18324  evlslem2  18378  evlslem3  18381  coe1tmmul2  18515  coe1tmmul  18516  cply1mul  18533  gsummoncoe1  18544  evls1gsumadd  18559  cnfldmulg  18648  cnsubmlem  18664  gsumfsum  18682  nn0srg  18684  rge0srg  18685  zring0  18696  re0g  18824  uvcresum  18998  mamudi  19075  mamudir  19076  mamulid  19113  mamurid  19114  mat1dimmul  19148  mat1mhm  19156  dmatmul  19169  scmatscm  19185  1mavmul  19220  mulmarep1gsum1  19245  mdet0pr  19264  m1detdiag  19269  mdetdiag  19271  mdet0  19278  m2detleib  19303  maducoeval2  19312  madugsum  19315  smadiadetlem1a  19335  smadiadetlem3  19340  smadiadet  19342  cpmatmcllem  19389  mat2pmatghm  19401  mat2pmatmul  19402  pmatcollpw3fi1lem1  19457  idpm2idmp  19472  mp2pm2mplem4  19480  pm2mpghm  19487  monmat2matmon  19495  pm2mp  19496  chfacfscmulgsum  19531  chfacfpmmulgsum  19535  cpmadugsumlemF  19547  cayhamlem4  19559  tdeglem4  22627  tdeglem2  22628  mdegmullem  22647  coe1mul3  22669  plypf1  22778  tayl0  22926  jensen  23519  amgmlem  23520  suborng  28043  xrge0slmod  28072  zringnm  28178  rezh  28189  2zrng0  33017  cznrng  33036  mgpsumz  33225  ply1mulgsumlem2  33260
  Copyright terms: Public domain W3C validator