Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mndidcl | Structured version Visualization version GIF version |
Description: The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
Ref | Expression |
---|---|
mndidcl.b | ⊢ 𝐵 = (Base‘𝐺) |
mndidcl.o | ⊢ 0 = (0g‘𝐺) |
Ref | Expression |
---|---|
mndidcl | ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mndidcl.b | . 2 ⊢ 𝐵 = (Base‘𝐺) | |
2 | mndidcl.o | . 2 ⊢ 0 = (0g‘𝐺) | |
3 | eqid 2821 | . 2 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | 1, 3 | mndid 17921 | . 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)) |
5 | 1, 2, 3, 4 | mgmidcl 17876 | 1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 ‘cfv 6355 Basecbs 16483 +gcplusg 16565 0gc0g 16713 Mndcmnd 17911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-iota 6314 df-fun 6357 df-fv 6363 df-riota 7114 df-ov 7159 df-0g 16715 df-mgm 17852 df-sgrp 17901 df-mnd 17912 |
This theorem is referenced by: mndbn0 17927 hashfinmndnn 17928 mndpfo 17934 prdsidlem 17943 imasmnd 17949 idmhm 17965 mhmf1o 17966 issubmd 17971 submid 17975 0subm 17982 0mhm 17984 mhmco 17988 mhmeql 17990 submacs 17991 mndind 17992 prdspjmhm 17993 pwsdiagmhm 17995 pwsco1mhm 17996 pwsco2mhm 17997 gsumvallem2 17998 dfgrp2 18128 grpidcl 18131 mhmid 18220 mhmmnd 18221 mulgnn0cl 18244 mulgnn0z 18254 cntzsubm 18466 oppgmnd 18482 gex1 18716 mulgnn0di 18946 mulgmhm 18948 subcmn 18957 gsumval3 19027 gsumzcl2 19030 gsumzaddlem 19041 gsumzsplit 19047 gsumzmhm 19057 gsummpt1n0 19085 simpgnideld 19221 srgidcl 19268 srg0cl 19269 ringidcl 19318 gsummgp0 19358 pwssplit1 19831 dsmm0cl 20884 dsmmacl 20885 mndvlid 21004 mndvrid 21005 mdet0 21215 mndifsplit 21245 gsummatr01lem3 21266 pmatcollpw3fi1lem1 21394 tmdmulg 22700 tmdgsum 22703 tsms0 22750 tsmssplit 22760 tsmsxp 22763 cntzsnid 30696 submomnd 30711 omndmul2 30713 omndmul3 30714 omndmul 30715 ogrpinv0le 30716 gsumle 30725 slmd0vcl 30849 sibf0 31592 sitmcl 31609 pwssplit4 39709 c0mgm 44200 c0mhm 44201 c0snmgmhm 44205 c0snmhm 44206 mgpsumz 44430 mndpsuppss 44439 lco0 44502 |
Copyright terms: Public domain | W3C validator |