| 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 2737 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
| 2 | eqid 2737 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
| 3 | 1, 2 | iscmn 19807 | . 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 1540 ∈ wcel 2108 ∀wral 3061 ‘cfv 6561 (class class class)co 7431 Basecbs 17247 +gcplusg 17297 Mndcmnd 18747 CMndccmn 19798 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 df-cmn 19800 |
| This theorem is referenced by: cmn32 19818 cmn4 19819 cmn12 19820 cmnmndd 19822 rinvmod 19824 mulgnn0di 19843 mulgmhm 19845 ghmcmn 19849 prdscmnd 19879 gsumres 19931 gsumcl2 19932 gsumf1o 19934 gsumsubmcl 19937 gsumadd 19941 gsumsplit 19946 gsummhm 19956 gsummulglem 19959 gsuminv 19964 gsumpr 19973 gsumunsnfd 19975 gsumdifsnd 19979 gsum2d 19990 prdsgsum 19999 srgmnd 20187 gsumvsmul 20924 frlmgsum 21792 frlmup2 21819 islindf4 21858 evlslem3 22104 mdetdiagid 22606 mdetrlin 22608 gsummatr01lem3 22663 gsummatr01 22665 chpscmat 22848 chp0mat 22852 chpidmat 22853 tmdgsum 24103 tmdgsum2 24104 tsms0 24150 tsmsmhm 24154 tsmsadd 24155 tgptsmscls 24158 tsmssplit 24160 tsmsxplem1 24161 tsmsxplem2 24162 imasdsf1olem 24383 lgseisenlem4 27422 xrge00 33017 gsumvsmul1 33054 gsummptres 33055 xrge0omnd 33088 gsumle 33101 slmdmnd 33212 lbsdiflsp0 33677 xrge0iifmhm 33938 xrge0tmdALT 33945 esum0 34050 esumsnf 34065 esumcocn 34081 aks6d1c1 42117 aks6d1c5lem0 42136 aks6d1c5lem3 42138 aks6d1c5lem2 42139 aks6d1c5 42140 gsumge0cl 46386 sge0tsms 46395 gsumdifsndf 48097 |
| Copyright terms: Public domain | W3C validator |