![]() |
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 2735 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2735 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | 1, 2 | iscmn 19822 | . 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 1537 ∈ wcel 2106 ∀wral 3059 ‘cfv 6563 (class class class)co 7431 Basecbs 17245 +gcplusg 17298 Mndcmnd 18760 CMndccmn 19813 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-iota 6516 df-fv 6571 df-ov 7434 df-cmn 19815 |
This theorem is referenced by: cmn32 19833 cmn4 19834 cmn12 19835 cmnmndd 19837 rinvmod 19839 mulgnn0di 19858 mulgmhm 19860 ghmcmn 19864 prdscmnd 19894 gsumres 19946 gsumcl2 19947 gsumf1o 19949 gsumsubmcl 19952 gsumadd 19956 gsumsplit 19961 gsummhm 19971 gsummulglem 19974 gsuminv 19979 gsumpr 19988 gsumunsnfd 19990 gsumdifsnd 19994 gsum2d 20005 prdsgsum 20014 srgmnd 20208 gsumvsmul 20941 frlmgsum 21810 frlmup2 21837 islindf4 21876 evlslem3 22122 mdetdiagid 22622 mdetrlin 22624 gsummatr01lem3 22679 gsummatr01 22681 chpscmat 22864 chp0mat 22868 chpidmat 22869 tmdgsum 24119 tmdgsum2 24120 tsms0 24166 tsmsmhm 24170 tsmsadd 24171 tgptsmscls 24174 tsmssplit 24176 tsmsxplem1 24177 tsmsxplem2 24178 imasdsf1olem 24399 lgseisenlem4 27437 xrge00 33000 gsumvsmul1 33037 gsummptres 33038 xrge0omnd 33071 gsumle 33084 slmdmnd 33195 lbsdiflsp0 33654 xrge0iifmhm 33900 xrge0tmdALT 33907 esum0 34030 esumsnf 34045 esumcocn 34061 aks6d1c1 42098 aks6d1c5lem0 42117 aks6d1c5lem3 42119 aks6d1c5lem2 42120 aks6d1c5 42121 gsumge0cl 46327 sge0tsms 46336 gsumdifsndf 48025 |
Copyright terms: Public domain | W3C validator |