![]() |
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 2734 | . 2 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | 1, 3 | mndid 18769 | . 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)) |
5 | 1, 2, 3, 4 | mgmidcl 18691 | 1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 ‘cfv 6562 Basecbs 17244 +gcplusg 17297 0gc0g 17485 Mndcmnd 18759 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-iota 6515 df-fun 6564 df-fv 6570 df-riota 7387 df-ov 7433 df-0g 17487 df-mgm 18665 df-sgrp 18744 df-mnd 18760 |
This theorem is referenced by: mndbn0 18775 hashfinmndnn 18776 mndpfo 18782 mndpsuppss 18790 prdsidlem 18794 imasmnd 18800 xpsmnd0 18803 idmhm 18820 mhmf1o 18821 mndvlid 18824 mndvrid 18825 issubmd 18831 submid 18835 0subm 18842 0mhm 18844 mhmco 18848 mhmeql 18851 submacs 18852 mndind 18853 prdspjmhm 18854 pwsdiagmhm 18856 pwsco1mhm 18857 pwsco2mhm 18858 gsumvallem2 18859 dfgrp2 18992 grpidcl 18995 mhmid 19093 mhmmnd 19094 mulgnn0cl 19120 mulgnn0z 19131 cntzsubm 19368 oppgmnd 19387 gex1 19623 mulgnn0di 19857 mulgmhm 19859 subcmn 19869 gsumval3 19939 gsumzcl2 19942 gsumzaddlem 19953 gsumzsplit 19959 gsumzmhm 19969 gsummpt1n0 19997 simpgnideld 20133 srgidcl 20216 srg0cl 20217 ringidcl 20279 gsummgp0 20331 c0mgm 20475 c0mhm 20476 c0snmgmhm 20478 c0snmhm 20479 pwssplit1 21075 rngqiprngimf1 21327 dsmm0cl 21777 dsmmacl 21778 mhmcompl 22399 mdet0 22627 mndifsplit 22657 gsummatr01lem3 22678 pmatcollpw3fi1lem1 22807 tmdmulg 24115 tmdgsum 24118 tsms0 24165 tsmssplit 24175 tsmsxp 24178 mndlactfo 33014 mndractfo 33016 mndlactf1o 33017 mndractf1o 33018 gsumwun 33050 cntzsnid 33054 submomnd 33069 omndmul2 33071 omndmul3 33072 omndmul 33073 ogrpinv0le 33074 gsumle 33083 slmd0vcl 33209 ply1degltdimlem 33649 lvecendof1f1o 33660 sibf0 34315 sitmcl 34332 primrootsunit1 42078 primrootscoprmpow 42080 primrootscoprbij 42083 evl1gprodd 42098 ringexp0nn 42115 aks6d1c5lem2 42119 pwssplit4 43077 mgpsumz 48206 lco0 48272 mndtccatid 48895 |
Copyright terms: Public domain | W3C validator |