![]() |
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 2735 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | eqid 2735 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
3 | eqid 2735 | . . 3 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
4 | 1, 2, 3 | isgrp 18970 | . 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺))) |
5 | 4 | simplbi 497 | 1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 ∀wral 3059 ∃wrex 3068 ‘cfv 6563 (class class class)co 7431 Basecbs 17245 +gcplusg 17298 0gc0g 17486 Mndcmnd 18760 Grpcgrp 18964 |
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-grp 18967 |
This theorem is referenced by: grpcl 18972 grpass 18973 grpideu 18975 grpmndd 18977 grpplusf 18979 grpplusfo 18980 grpsgrp 18991 dfgrp2 18993 grpidcl 18996 grplid 18998 grprid 18999 dfgrp3 19070 prdsgrpd 19081 prdsinvgd 19082 mulgaddcom 19129 mulginvcom 19130 mulgz 19133 mulgneg2 19139 mulgass 19142 issubg3 19175 grpissubg 19177 0subg 19182 subgacs 19192 0ghm 19261 pwsdiagghm 19275 cntzsubg 19370 oppggrp 19391 symgsubmefmndALT 19436 psgnunilem5 19527 psgnuni 19532 0subgALT 19601 lsmcntzr 19713 pj1ghm 19736 isabl2 19823 cntrabl 19876 dprdfid 20052 dprdfeq0 20057 dprdlub 20061 dmdprdsplitlem 20072 dprddisj2 20074 dpjidcl 20093 pgpfaclem3 20118 simpgnideld 20134 c0ghm 20478 c0snghm 20481 dsmmsubg 21781 frlm0 21792 mdetunilem7 22640 istgp2 24115 cyc3genpm 33155 isarchi3 33177 reofld 33352 lbslsat 33644 dimkerim 33655 fedgmullem2 33658 primrootscoprbij 42084 grpods 42176 pwssplit4 43078 pwslnmlem2 43082 lcoel0 48274 |
Copyright terms: Public domain | W3C validator |