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 2610 | . 2 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | 1, 3 | mndid 17126 | . 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)) |
5 | 1, 2, 3, 4 | mgmidcl 17088 | 1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ‘cfv 5804 Basecbs 15695 +gcplusg 15768 0gc0g 15923 Mndcmnd 17117 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-iota 5768 df-fun 5806 df-fv 5812 df-riota 6511 df-ov 6552 df-0g 15925 df-mgm 17065 df-sgrp 17107 df-mnd 17118 |
This theorem is referenced by: mndpfo 17137 prdsidlem 17145 imasmnd 17151 idmhm 17167 mhmf1o 17168 issubmd 17172 submid 17174 0mhm 17181 mhmco 17185 mhmeql 17187 submacs 17188 mrcmndind 17189 prdspjmhm 17190 pwsdiagmhm 17192 pwsco1mhm 17193 pwsco2mhm 17194 gsumvallem2 17195 dfgrp2 17270 grpidcl 17273 mhmid 17359 mhmmnd 17360 mulgnn0cl 17381 mulgnn0z 17390 cntzsubm 17591 oppgmnd 17607 gex1 17829 mulgnn0di 18054 mulgmhm 18056 subcmn 18065 gsumval3 18131 gsumzcl2 18134 gsumzaddlem 18144 gsumzsplit 18150 gsumzmhm 18160 gsummpt1n0 18187 srgidcl 18341 srg0cl 18342 ringidcl 18391 gsummgp0 18431 pwssplit1 18880 dsmm0cl 19903 dsmmacl 19904 mndvlid 20018 mndvrid 20019 mdet0 20231 mndifsplit 20261 gsummatr01lem3 20282 pmatcollpw3fi1lem1 20410 tmdmulg 21706 tmdgsum 21709 tsms0 21755 tsmssplit 21765 tsmsxp 21768 submomnd 29041 omndmul2 29043 omndmul3 29044 omndmul 29045 ogrpinv0le 29047 slmdbn0 29092 slmdsn0 29095 slmd0vcl 29105 gsumle 29110 sibf0 29723 sitmcl 29740 pwssplit4 36677 c0mgm 41699 c0mhm 41700 c0snmgmhm 41704 c0snmhm 41705 mgpsumz 41934 mndpsuppss 41946 lco0 42010 |
Copyright terms: Public domain | W3C validator |