![]() |
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 2733 | . 2 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | 1, 3 | mndid 18571 | . 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)) |
5 | 1, 2, 3, 4 | mgmidcl 18526 | 1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ‘cfv 6497 Basecbs 17088 +gcplusg 17138 0gc0g 17326 Mndcmnd 18561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3741 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-iota 6449 df-fun 6499 df-fv 6505 df-riota 7314 df-ov 7361 df-0g 17328 df-mgm 18502 df-sgrp 18551 df-mnd 18562 |
This theorem is referenced by: mndbn0 18577 hashfinmndnn 18578 mndpfo 18584 prdsidlem 18593 imasmnd 18599 idmhm 18616 mhmf1o 18617 issubmd 18622 submid 18626 0subm 18633 0mhm 18635 mhmco 18639 mhmeql 18641 submacs 18642 mndind 18643 prdspjmhm 18644 pwsdiagmhm 18646 pwsco1mhm 18647 pwsco2mhm 18648 gsumvallem2 18649 dfgrp2 18780 grpidcl 18783 mhmid 18873 mhmmnd 18874 mulgnn0cl 18897 mulgnn0z 18908 cntzsubm 19121 oppgmnd 19140 gex1 19378 mulgnn0di 19609 mulgmhm 19611 subcmn 19620 gsumval3 19689 gsumzcl2 19692 gsumzaddlem 19703 gsumzsplit 19709 gsumzmhm 19719 gsummpt1n0 19747 simpgnideld 19883 srgidcl 19935 srg0cl 19936 ringidcl 19994 gsummgp0 20037 pwssplit1 20535 dsmm0cl 21162 dsmmacl 21163 mndvlid 21758 mndvrid 21759 mdet0 21971 mndifsplit 22001 gsummatr01lem3 22022 pmatcollpw3fi1lem1 22151 tmdmulg 23459 tmdgsum 23462 tsms0 23509 tsmssplit 23519 tsmsxp 23522 cntzsnid 31952 submomnd 31967 omndmul2 31969 omndmul3 31970 omndmul 31971 ogrpinv0le 31972 gsumle 31981 slmd0vcl 32105 ply1degltdimlem 32374 sibf0 32991 sitmcl 33008 mhmcompl 40779 pwssplit4 41459 c0mgm 46293 c0mhm 46294 c0snmgmhm 46298 c0snmhm 46299 mgpsumz 46524 mndpsuppss 46533 lco0 46594 mndtccatid 47199 |
Copyright terms: Public domain | W3C validator |