Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > grpmnd | Structured version Visualization version GIF version |
Description: A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
Ref | Expression |
---|---|
grpmnd | ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2610 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2610 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | eqid 2610 | . . 3 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
4 | 1, 2, 3 | isgrp 17251 | . 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺))) |
5 | 4 | simplbi 475 | 1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 ‘cfv 5804 (class class class)co 6549 Basecbs 15695 +gcplusg 15768 0gc0g 15923 Mndcmnd 17117 Grpcgrp 17245 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 df-grp 17248 |
This theorem is referenced by: grpcl 17253 grpass 17254 grpideu 17256 grpplusf 17257 grpplusfo 17258 grpsgrp 17269 dfgrp2 17270 grpidcl 17273 grplid 17275 grprid 17276 dfgrp3 17337 prdsgrpd 17348 prdsinvgd 17349 ghmgrp 17362 mulgaddcom 17387 mulginvcom 17388 mulgz 17391 mulgdirlem 17395 mulgneg2 17398 mulgass 17402 issubg3 17435 subgacs 17452 ghmmhm 17493 0ghm 17497 pwsdiagghm 17511 cntzsubg 17592 oppggrp 17610 gsumccatsymgsn 17669 symggen 17713 symgtrinv 17715 psgnunilem5 17737 psgnunilem2 17738 psgnuni 17742 psgneldm2 17747 psgnfitr 17760 lsmass 17906 lsmcntzr 17916 pj1ghm 17939 frgpmhm 18001 frgpuplem 18008 frgpupf 18009 frgpup1 18011 isabl2 18024 isabld 18029 gsumzinv 18168 telgsumfzslem 18208 telgsumfzs 18209 dprdssv 18238 dprdfid 18239 dprdfadd 18242 dprdfeq0 18244 dprdlub 18248 dmdprdsplitlem 18259 dprddisj2 18261 dpjidcl 18280 pgpfac1lem3a 18298 pgpfaclem3 18305 ringmnd 18379 unitabl 18491 unitsubm 18493 lmodvsmmulgdi 18721 psgnghm 19745 dsmmsubg 19906 frlm0 19917 mdetunilem7 20243 istgp2 21705 symgtgp 21715 clmmulg 22709 dchrptlem3 24791 abliso 29027 isarchi3 29072 ofldchr 29145 reofld 29171 pwssplit4 36677 pwslnmlem2 36681 gicabl 36687 mendring 36781 c0ghm 41701 c0snghm 41706 lmodvsmdi 41957 lincvalsng 41999 lincvalsc0 42004 linc0scn0 42006 linc1 42008 lcoel0 42011 lincsum 42012 lincsumcl 42014 snlindsntor 42054 |
Copyright terms: Public domain | W3C validator |