![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ringmnd | Structured version Visualization version GIF version |
Description: A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Ref | Expression |
---|---|
ringmnd | ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringgrp 18913 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | grpmnd 17790 | . 2 ⊢ (𝑅 ∈ Grp → 𝑅 ∈ Mnd) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2164 Mndcmnd 17654 Grpcgrp 17783 Ringcrg 18908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-nul 5015 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-uni 4661 df-br 4876 df-iota 6090 df-fv 6135 df-ov 6913 df-grp 17786 df-ring 18910 |
This theorem is referenced by: ringmgm 18918 gsummulc1 18967 gsummulc2 18968 gsummgp0 18969 prdsringd 18973 pwsco1rhm 19101 lmodvsmmulgdi 19261 psrlidm 19771 psrridm 19772 mplsubrglem 19807 mplmonmul 19832 evlslem2 19879 evlslem3 19881 coe1tmmul2 20013 coe1tmmul 20014 cply1mul 20031 gsummoncoe1 20041 evls1gsumadd 20056 cnfldmulg 20145 cnsubmlem 20161 gsumfsum 20180 nn0srg 20183 rge0srg 20184 zring0 20195 re0g 20326 uvcresum 20506 mamudi 20583 mamudir 20584 mamulid 20621 mamurid 20622 mat1dimmul 20657 mat1mhm 20665 dmatmul 20678 scmatscm 20694 1mavmul 20729 mulmarep1gsum1 20754 mdet0pr 20773 m1detdiag 20778 mdetdiag 20780 mdet0 20787 m2detleib 20812 maducoeval2 20821 madugsum 20824 smadiadetlem1a 20845 smadiadetlem3 20850 smadiadet 20852 cpmatmcllem 20900 mat2pmatghm 20912 mat2pmatmul 20913 pmatcollpw3fi1lem1 20968 idpm2idmp 20983 mp2pm2mplem4 20991 pm2mpghm 20998 monmat2matmon 21006 pm2mp 21007 chfacfscmulgsum 21042 chfacfpmmulgsum 21046 cpmadugsumlemF 21058 cayhamlem4 21070 tdeglem4 24226 tdeglem2 24227 mdegmullem 24244 coe1mul3 24265 plypf1 24374 tayl0 24522 jensen 25135 amgmlem 25136 suborng 30356 xrge0slmod 30385 zringnm 30545 rezh 30556 amgm2d 39336 amgm3d 39337 amgm4d 39338 2zrng0 42799 cznrng 42816 mgpsumz 43002 ply1mulgsumlem2 43036 amgmwlem 43454 amgmw2d 43456 |
Copyright terms: Public domain | W3C validator |