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 19231 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | grpmnd 18048 | . 2 ⊢ (𝑅 ∈ Grp → 𝑅 ∈ Mnd) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 Mndcmnd 17899 Grpcgrp 18041 Ringcrg 19226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-nul 5201 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 df-grp 18044 df-ring 19228 |
This theorem is referenced by: ringmgm 19236 gsummulc1 19285 gsummulc2 19286 gsummgp0 19287 prdsringd 19291 pwsco1rhm 19419 lmodvsmmulgdi 19598 psrlidm 20111 psrridm 20112 mplsubrglem 20147 mplmonmul 20173 evlslem2 20220 evlslem3 20221 evlsgsumadd 20232 coe1tmmul2 20372 coe1tmmul 20373 cply1mul 20390 gsummoncoe1 20400 evls1gsumadd 20415 cnfldmulg 20505 cnsubmlem 20521 gsumfsum 20540 nn0srg 20543 rge0srg 20544 zring0 20555 re0g 20684 uvcresum 20865 mamudi 20940 mamudir 20941 mamulid 20978 mamurid 20979 mat1dimmul 21013 mat1mhm 21021 dmatmul 21034 scmatscm 21050 1mavmul 21085 mulmarep1gsum1 21110 mdet0pr 21129 m1detdiag 21134 mdetdiag 21136 mdet0 21143 m2detleib 21168 maducoeval2 21177 madugsum 21180 smadiadetlem1a 21200 smadiadetlem3 21205 smadiadet 21207 cpmatmcllem 21254 mat2pmatghm 21266 mat2pmatmul 21267 pmatcollpw3fi1lem1 21322 idpm2idmp 21337 mp2pm2mplem4 21345 pm2mpghm 21352 monmat2matmon 21360 pm2mp 21361 chfacfscmulgsum 21396 chfacfpmmulgsum 21400 cpmadugsumlemF 21412 cayhamlem4 21424 tdeglem4 24581 tdeglem2 24582 mdegmullem 24599 coe1mul3 24620 plypf1 24729 tayl0 24877 jensen 25493 amgmlem 25494 freshmansdream 30786 suborng 30815 xrge0slmod 30844 drgext0gsca 30893 fedgmullem2 30925 extdg1id 30952 zringnm 31100 rezh 31111 amgm2d 40429 amgm3d 40430 amgm4d 40431 2zrng0 44137 cznrng 44154 mgpsumz 44338 ply1mulgsumlem2 44369 amgmwlem 44831 amgmw2d 44833 |
Copyright terms: Public domain | W3C validator |