![]() |
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 2793 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2793 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | eqid 2793 | . . 3 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
4 | 1, 2, 3 | isgrp 17855 | . 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺))) |
5 | 4 | simplbi 498 | 1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1520 ∈ wcel 2079 ∀wral 3103 ∃wrex 3104 ‘cfv 6217 (class class class)co 7007 Basecbs 16300 +gcplusg 16382 0gc0g 16530 Mndcmnd 17721 Grpcgrp 17849 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-iota 6181 df-fv 6225 df-ov 7010 df-grp 17852 |
This theorem is referenced by: grpcl 17857 grpass 17858 grpideu 17860 grpplusf 17861 grpplusfo 17862 grpsgrp 17873 dfgrp2 17874 grpidcl 17877 grplid 17879 grprid 17880 dfgrp3 17943 prdsgrpd 17954 prdsinvgd 17955 ghmgrp 17968 mulgaddcom 17993 mulginvcom 17994 mulgz 17997 mulgdirlem 18000 mulgneg2 18003 mulgass 18006 issubg3 18039 subgacs 18056 ghmmhm 18097 0ghm 18101 pwsdiagghm 18115 cntzsubg 18196 oppggrp 18214 gsumccatsymgsn 18273 symggen 18317 symgtrinv 18319 psgnunilem5 18341 psgnunilem2 18342 psgnuni 18346 psgneldm2 18351 psgnfitr 18364 lsmass 18511 lsmcntzr 18521 pj1ghm 18544 frgpmhm 18606 frgpuplem 18613 frgpupf 18614 frgpup1 18616 isabl2 18629 isabld 18634 gsumzinv 18773 telgsumfzslem 18813 telgsumfzs 18814 dprdssv 18843 dprdfid 18844 dprdfadd 18847 dprdfeq0 18849 dprdlub 18853 dmdprdsplitlem 18864 dprddisj2 18866 dpjidcl 18885 pgpfac1lem3a 18903 pgpfaclem3 18910 ringmnd 18984 unitabl 19096 unitsubm 19098 lmodvsmmulgdi 19347 psgnghm 20394 dsmmsubg 20557 frlm0 20568 mdetunilem7 20899 istgp2 22371 symgtgp 22381 clmmulg 23376 dchrptlem3 25512 abliso 30327 cyc3genpmlem 30389 cyc3genpm 30390 isarchi3 30412 cntrabl 30464 ofldchr 30496 reofld 30522 lbslsat 30573 dimkerim 30582 fedgmullem2 30585 pwssplit4 39125 pwslnmlem2 39129 gicabl 39135 mendring 39228 hashfingrpnn 40097 simpgnideld 40107 c0ghm 43614 c0snghm 43619 lmodvsmdi 43864 lincvalsng 43905 lincvalsc0 43910 linc0scn0 43912 linc1 43914 lcoel0 43917 lincsum 43918 lincsumcl 43920 snlindsntor 43960 |
Copyright terms: Public domain | W3C validator |