Theorem mndidcl 18657

Description: The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)

Hypotheses

Ref	Expression
mndidcl.b	⊢ 𝐵 = (Base‘𝐺)
mndidcl.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
mndidcl	⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Proof of Theorem mndidcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mndidcl.b	. 2 ⊢ 𝐵 = (Base‘𝐺)
2		mndidcl.o	. 2 ⊢ 0 = (0g‘𝐺)
3		eqid 2731	. 2 ⊢ (+g‘𝐺) = (+g‘𝐺)
4	1, 3	mndid 18652	. 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦))
5	1, 2, 3, 4	mgmidcl 18574	1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  Basecbs 17120  +_gcplusg 17161  0_gc0g 17343  Mndcmnd 18642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6437  df-fun 6483  df-fv 6489  df-riota 7303  df-ov 7349  df-0g 17345  df-mgm 18548  df-sgrp 18627  df-mnd 18643

This theorem is referenced by:  mndbn0  18658  hashfinmndnn  18659  mndpfo  18665  mndpsuppss  18673  prdsidlem  18677  imasmnd  18683  xpsmnd0  18686  idmhm  18703  mhmf1o  18704  mndvlid  18707  mndvrid  18708  issubmd  18714  submid  18718  0subm  18725  0mhm  18727  mhmco  18731  mhmeql  18734  submacs  18735  mndind  18736  prdspjmhm  18737  pwsdiagmhm  18739  pwsco1mhm  18740  pwsco2mhm  18741  gsumvallem2  18742  dfgrp2  18875  grpidcl  18878  mhmid  18976  mhmmnd  18977  mulgnn0cl  19003  mulgnn0z  19014  cntzsubm  19250  oppgmnd  19266  gex1  19503  mulgnn0di  19737  mulgmhm  19739  subcmn  19749  gsumval3  19819  gsumzcl2  19822  gsumzaddlem  19833  gsumzsplit  19839  gsumzmhm  19849  gsummpt1n0  19877  simpgnideld  20013  submomnd  20044  omndmul2  20045  omndmul3  20046  omndmul  20047  ogrpinv0le  20048  gsumle  20057  srgidcl  20117  srg0cl  20118  ringidcl  20183  gsummgp0  20236  c0mgm  20377  c0mhm  20378  c0snmgmhm  20380  c0snmhm  20381  pwssplit1  20993  rngqiprngimf1  21237  dsmm0cl  21677  dsmmacl  21678  mhmcompl  22295  mdet0  22521  mndifsplit  22551  gsummatr01lem3  22572  pmatcollpw3fi1lem1  22701  tmdmulg  24007  tmdgsum  24010  tsms0  24057  tsmssplit  24067  tsmsxp  24070  mndlactfo  33008  mndractfo  33010  mndlactf1o  33011  mndractf1o  33012  gsumwun  33045  cntzsnid  33049  fxpsubm  33141  slmd0vcl  33190  ply1degltdimlem  33635  lvecendof1f1o  33646  sibf0  34347  sitmcl  34364  primrootsunit1  42200  primrootscoprmpow  42202  primrootscoprbij  42205  evl1gprodd  42220  ringexp0nn  42237  aks6d1c5lem2  42241  pwssplit4  43192  mgpsumz  48472  lco0  48538  mndtccatid  49698