![]() |
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 2651 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2651 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | eqid 2651 | . . 3 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
4 | 1, 2, 3 | isgrp 17475 | . 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 1523 ∈ wcel 2030 ∀wral 2941 ∃wrex 2942 ‘cfv 5926 (class class class)co 6690 Basecbs 15904 +gcplusg 15988 0gc0g 16147 Mndcmnd 17341 Grpcgrp 17469 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-grp 17472 |
This theorem is referenced by: grpcl 17477 grpass 17478 grpideu 17480 grpplusf 17481 grpplusfo 17482 grpsgrp 17493 dfgrp2 17494 grpidcl 17497 grplid 17499 grprid 17500 dfgrp3 17561 prdsgrpd 17572 prdsinvgd 17573 ghmgrp 17586 mulgaddcom 17611 mulginvcom 17612 mulgz 17615 mulgdirlem 17619 mulgneg2 17622 mulgass 17626 issubg3 17659 subgacs 17676 ghmmhm 17717 0ghm 17721 pwsdiagghm 17735 cntzsubg 17815 oppggrp 17833 gsumccatsymgsn 17892 symggen 17936 symgtrinv 17938 psgnunilem5 17960 psgnunilem2 17961 psgnuni 17965 psgneldm2 17970 psgnfitr 17983 lsmass 18129 lsmcntzr 18139 pj1ghm 18162 frgpmhm 18224 frgpuplem 18231 frgpupf 18232 frgpup1 18234 isabl2 18247 isabld 18252 gsumzinv 18391 telgsumfzslem 18431 telgsumfzs 18432 dprdssv 18461 dprdfid 18462 dprdfadd 18465 dprdfeq0 18467 dprdlub 18471 dmdprdsplitlem 18482 dprddisj2 18484 dpjidcl 18503 pgpfac1lem3a 18521 pgpfaclem3 18528 ringmnd 18602 unitabl 18714 unitsubm 18716 lmodvsmmulgdi 18946 psgnghm 19974 dsmmsubg 20135 frlm0 20146 mdetunilem7 20472 istgp2 21942 symgtgp 21952 clmmulg 22947 dchrptlem3 25036 abliso 29824 isarchi3 29869 ofldchr 29942 reofld 29968 pwssplit4 37976 pwslnmlem2 37980 gicabl 37986 mendring 38079 c0ghm 42236 c0snghm 42241 lmodvsmdi 42488 lincvalsng 42530 lincvalsc0 42535 linc0scn0 42537 linc1 42539 lcoel0 42542 lincsum 42543 lincsumcl 42545 snlindsntor 42585 |
Copyright terms: Public domain | W3C validator |