![]() |
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 2728 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2728 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | 1, 2 | iscmn 19744 | . 2 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥))) |
4 | 3 | simplbi 497 | 1 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 ∀wral 3058 ‘cfv 6548 (class class class)co 7420 Basecbs 17180 +gcplusg 17233 Mndcmnd 18694 CMndccmn 19735 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-cmn 19737 |
This theorem is referenced by: cmn32 19755 cmn4 19756 cmn12 19757 cmnmndd 19759 rinvmod 19761 mulgnn0di 19780 mulgmhm 19782 ghmcmn 19786 prdscmnd 19816 gsumres 19868 gsumcl2 19869 gsumf1o 19871 gsumsubmcl 19874 gsumadd 19878 gsumsplit 19883 gsummhm 19893 gsummulglem 19896 gsuminv 19901 gsumpr 19910 gsumunsnfd 19912 gsumdifsnd 19916 gsum2d 19927 prdsgsum 19936 srgmnd 20130 gsumvsmul 20809 frlmgsum 21706 frlmup2 21733 islindf4 21772 evlslem3 22026 mdetdiagid 22515 mdetrlin 22517 gsummatr01lem3 22572 gsummatr01 22574 chpscmat 22757 chp0mat 22761 chpidmat 22762 tmdgsum 24012 tmdgsum2 24013 tsms0 24059 tsmsmhm 24063 tsmsadd 24064 tgptsmscls 24067 tsmssplit 24069 tsmsxplem1 24070 tsmsxplem2 24071 imasdsf1olem 24292 lgseisenlem4 27324 xrge00 32755 gsumvsmul1 32778 gsummptres 32779 xrge0omnd 32804 gsumle 32817 slmdmnd 32926 lbsdiflsp0 33324 xrge0iifmhm 33540 xrge0tmdALT 33547 esum0 33668 esumsnf 33683 esumcocn 33699 aks6d1c1 41587 aks6d1c5lem0 41606 aks6d1c5lem3 41608 aks6d1c5lem2 41609 aks6d1c5 41610 gsumge0cl 45759 sge0tsms 45768 gsumdifsndf 47243 |
Copyright terms: Public domain | W3C validator |