![]() |
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 2725 | . 2 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | 1, 3 | mndid 18707 | . 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)) |
5 | 1, 2, 3, 4 | mgmidcl 18629 | 1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ‘cfv 6549 Basecbs 17183 +gcplusg 17236 0gc0g 17424 Mndcmnd 18697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-iota 6501 df-fun 6551 df-fv 6557 df-riota 7375 df-ov 7422 df-0g 17426 df-mgm 18603 df-sgrp 18682 df-mnd 18698 |
This theorem is referenced by: mndbn0 18713 hashfinmndnn 18714 mndpfo 18720 prdsidlem 18729 imasmnd 18735 xpsmnd0 18738 idmhm 18755 mhmf1o 18756 mndvlid 18759 mndvrid 18760 issubmd 18766 submid 18770 0subm 18777 0mhm 18779 mhmco 18783 mhmeql 18786 submacs 18787 mndind 18788 prdspjmhm 18789 pwsdiagmhm 18791 pwsco1mhm 18792 pwsco2mhm 18793 gsumvallem2 18794 dfgrp2 18927 grpidcl 18930 mhmid 19027 mhmmnd 19028 mulgnn0cl 19053 mulgnn0z 19064 cntzsubm 19301 oppgmnd 19320 gex1 19558 mulgnn0di 19792 mulgmhm 19794 subcmn 19804 gsumval3 19874 gsumzcl2 19877 gsumzaddlem 19888 gsumzsplit 19894 gsumzmhm 19904 gsummpt1n0 19932 simpgnideld 20068 srgidcl 20151 srg0cl 20152 ringidcl 20214 gsummgp0 20266 c0mgm 20410 c0mhm 20411 c0snmgmhm 20413 c0snmhm 20414 pwssplit1 20956 rngqiprngimf1 21207 dsmm0cl 21691 dsmmacl 21692 mhmcompl 22324 mdet0 22552 mndifsplit 22582 gsummatr01lem3 22603 pmatcollpw3fi1lem1 22732 tmdmulg 24040 tmdgsum 24043 tsms0 24090 tsmssplit 24100 tsmsxp 24103 cntzsnid 32865 submomnd 32880 omndmul2 32882 omndmul3 32883 omndmul 32884 ogrpinv0le 32885 gsumle 32894 slmd0vcl 33020 ply1degltdimlem 33451 sibf0 34085 sitmcl 34102 primrootsunit1 41699 primrootscoprmpow 41702 primrootscoprbij 41705 evl1gprodd 41720 ringexp0nn 41737 aks6d1c5lem2 41741 pwssplit4 42655 mgpsumz 47612 mndpsuppss 47621 lco0 47681 mndtccatid 48285 |
Copyright terms: Public domain | W3C validator |