![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cmnmnd | Structured version Visualization version GIF version |
Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
Ref | Expression |
---|---|
cmnmnd | ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2800 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2800 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | 1, 2 | iscmn 18514 | . 2 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))) |
4 | 3 | simplbi 492 | 1 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 ∀wral 3090 ‘cfv 6102 (class class class)co 6879 Basecbs 16183 +gcplusg 16266 Mndcmnd 17608 CMndccmn 18507 |
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 2378 ax-ext 2778 |
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-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3388 df-dif 3773 df-un 3775 df-in 3777 df-ss 3784 df-nul 4117 df-if 4279 df-sn 4370 df-pr 4372 df-op 4376 df-uni 4630 df-br 4845 df-iota 6065 df-fv 6110 df-ov 6882 df-cmn 18509 |
This theorem is referenced by: cmn32 18525 cmn4 18526 cmn12 18527 mulgnn0di 18545 mulgmhm 18547 ghmcmn 18551 prdscmnd 18578 gsumres 18628 gsumcl2 18629 gsumf1o 18631 gsumsubmcl 18633 gsumadd 18637 gsumsplit 18642 gsummhm 18652 gsummulglem 18655 gsuminv 18660 gsumunsnfd 18670 gsumdifsnd 18674 gsum2d 18685 prdsgsum 18691 srgmnd 18824 gsumvsmul 19244 psrbagev1 19831 evlslem3 19835 evlslem1 19836 frlmgsum 20435 frlmup2 20462 islindf4 20501 mdetdiagid 20731 mdetrlin 20733 mdetrsca 20734 gsummatr01lem3 20789 gsummatr01 20791 chpscmat 20974 chp0mat 20978 chpidmat 20979 tmdgsum 22226 tmdgsum2 22227 tsms0 22272 tsmsmhm 22276 tsmsadd 22277 tgptsmscls 22280 tsmssplit 22282 tsmsxplem1 22283 tsmsxplem2 22284 imasdsf1olem 22505 lgseisenlem4 25454 xrge00 30201 xrge0omnd 30226 slmdmnd 30274 gsumle 30294 gsummptres 30299 xrge0iifmhm 30500 xrge0tmdOLD 30506 esum0 30626 esumsnf 30641 esumcocn 30657 gsumge0cl 41326 sge0tsms 41335 gsumpr 42933 gsumdifsndf 42938 |
Copyright terms: Public domain | W3C validator |