![]() |
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 18868 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | grpmnd 17745 | . 2 ⊢ (𝑅 ∈ Grp → 𝑅 ∈ Mnd) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 Mndcmnd 17609 Grpcgrp 17738 Ringcrg 18863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-nul 4983 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-iota 6064 df-fv 6109 df-ov 6881 df-grp 17741 df-ring 18865 |
This theorem is referenced by: ringmgm 18873 gsummulc1 18922 gsummulc2 18923 gsummgp0 18924 prdsringd 18928 pwsco1rhm 19056 lmodvsmmulgdi 19216 psrlidm 19726 psrridm 19727 mplsubrglem 19762 mplmonmul 19787 evlslem2 19834 evlslem3 19836 coe1tmmul2 19968 coe1tmmul 19969 cply1mul 19986 gsummoncoe1 19996 evls1gsumadd 20011 cnfldmulg 20100 cnsubmlem 20116 gsumfsum 20135 nn0srg 20138 rge0srg 20139 zring0 20150 re0g 20281 uvcresum 20457 mamudi 20534 mamudir 20535 mamulid 20572 mamurid 20573 mat1dimmul 20608 mat1mhm 20616 dmatmul 20629 scmatscm 20645 1mavmul 20680 mulmarep1gsum1 20705 mdet0pr 20724 m1detdiag 20729 mdetdiag 20731 mdet0 20738 m2detleib 20763 maducoeval2 20772 madugsum 20775 smadiadetlem1a 20796 smadiadetlem3 20801 smadiadet 20803 cpmatmcllem 20851 mat2pmatghm 20863 mat2pmatmul 20864 pmatcollpw3fi1lem1 20919 idpm2idmp 20934 mp2pm2mplem4 20942 pm2mpghm 20949 monmat2matmon 20957 pm2mp 20958 chfacfscmulgsum 20993 chfacfpmmulgsum 20997 cpmadugsumlemF 21009 cayhamlem4 21021 tdeglem4 24161 tdeglem2 24162 mdegmullem 24179 coe1mul3 24200 plypf1 24309 tayl0 24457 jensen 25067 amgmlem 25068 suborng 30331 xrge0slmod 30360 zringnm 30520 rezh 30531 amgm2d 39279 amgm3d 39280 amgm4d 39281 2zrng0 42733 cznrng 42750 mgpsumz 42936 ply1mulgsumlem2 42970 amgmwlem 43346 amgmw2d 43348 |
Copyright terms: Public domain | W3C validator |