![]() |
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 2795 | . 2 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | 1, 3 | mndid 17747 | . 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)) |
5 | 1, 2, 3, 4 | mgmidcl 17709 | 1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ∈ wcel 2081 ‘cfv 6230 Basecbs 16317 +gcplusg 16399 0gc0g 16547 Mndcmnd 17738 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3710 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-iota 6194 df-fun 6232 df-fv 6238 df-riota 6982 df-ov 7024 df-0g 16549 df-mgm 17686 df-sgrp 17728 df-mnd 17739 |
This theorem is referenced by: mndpfo 17758 prdsidlem 17766 imasmnd 17772 idmhm 17788 mhmf1o 17789 issubmd 17793 submid 17795 0mhm 17802 mhmco 17806 mhmeql 17808 submacs 17809 mndind 17810 prdspjmhm 17811 pwsdiagmhm 17813 pwsco1mhm 17814 pwsco2mhm 17815 gsumvallem2 17816 dfgrp2 17891 grpidcl 17894 mhmid 17982 mhmmnd 17983 mulgnn0cl 18004 mulgnn0z 18013 cntzsubm 18212 oppgmnd 18228 gex1 18451 mulgnn0di 18676 mulgmhm 18678 subcmn 18687 gsumval3 18753 gsumzcl2 18756 gsumzaddlem 18766 gsumzsplit 18772 gsumzmhm 18782 gsummpt1n0 18810 srgidcl 18963 srg0cl 18964 ringidcl 19013 gsummgp0 19053 pwssplit1 19526 dsmm0cl 20571 dsmmacl 20572 mndvlid 20691 mndvrid 20692 mdet0 20904 mndifsplit 20934 gsummatr01lem3 20955 pmatcollpw3fi1lem1 21083 tmdmulg 22389 tmdgsum 22392 tsms0 22438 tsmssplit 22448 tsmsxp 22451 submomnd 30376 omndmul2 30378 omndmul3 30379 omndmul 30380 ogrpinv0le 30381 slmdbn0 30479 slmdsn0 30482 slmd0vcl 30492 gsumle 30499 cntzsnid 30512 sibf0 31214 sitmcl 31231 pwssplit4 39199 hashfinmndnn 40169 simpgnideld 40180 c0mgm 43684 c0mhm 43685 c0snmgmhm 43689 c0snmhm 43690 mgpsumz 43914 mndpsuppss 43925 lco0 43988 |
Copyright terms: Public domain | W3C validator |