Theorem mndidcl 18853

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 2760	. 2 ⊢ (+g‘𝐺) = (+g‘𝐺)
4	1, 3	mndid 18847	. 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦))
5	1, 2, 3, 4	mgmidcl 18760	1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  Basecbs 17302  +_gcplusg 17343  0_gc0g 17525  Mndcmnd 18837

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-riota 7371  df-ov 7417  df-0g 17527  df-mgm 18731  df-sgrp 18822  df-mnd 18838

This theorem is used by:  mndbn0  18854  hashfinmndnn  18855  mndpfoOLD  18863  mndpsuppss  18873  prdsidlem  18877  imasmnd  18883  xpsmnd0  18886  idmhm  18904  mhmf1o  18905  mndvlid  18908  mndvrid  18909  issubmd  18915  submid  18919  0subm  18927  0mhm  18929  mhmco  18933  mhmeql  18936  submacs  18937  mndind  18938  prdspjmhm  18939  pwsdiagmhm  18941  pwsco1mhm  18942  pwsco2mhm  18943  gsumvallem2  18944  dfgrp2  19087  grpidcl  19090  mhmid  19187  mhmmnd  19188  mulgnn0cl  19214  mulgnn0z  19225  cntzsubm  19466  oppgmnd  19482  gex1  19719  mulgnn0di  19953  mulgmhm  19955  subcmn  19965  gsumval3  20035  gsumzcl2  20038  gsumzaddlem  20049  gsumzsplit  20055  gsumzmhm  20065  gsummpt1n0  20093  simpgnideld  20229  submomnd  20260  omndmul2  20261  omndmul3  20262  omndmul  20263  ogrpinv0le  20264  gsumle  20273  srgidcl  20339  srg0cl  20340  ringidcl  20407  gsummgp0  20459  c0mgm  20601  c0mhm  20602  c0snmgmhm  20604  c0snmhm  20605  pwssplit1  21244  rngqiprngimf1  21504  dsmm0cl  21954  dsmmacl  21955  mhmcompl  22338  mdet0  22829  mndifsplit  22859  gsummatr01lem3  22880  pmatcollpw3fi1lem1  23012  tmdmulg  24319  tmdgsum  24322  tsms0  24369  tsmssplit  24379  tsmsxp  24382  mndlactfo  33468  mndractfo  33470  mndlactf1o  33471  mndractf1o  33472  suppgsumssiun  33513  gsumwun  33517  cntzsnid  33521  fxpsubm  33613  slmd0vcl  33662  ply1degltdimlem  34133  lvecendof1f1o  34144  sibf0  34846  sitmcl  34863  primrootsunit1  42964  primrootscoprmpow  42966  primrootscoprbij  42969  evl1gprodd  42984  ringexp0nn  43001  aks6d1c5lem2  43005  pwssplit4  43931  mgpsumz  49293  lco0  49358  mndtccatid  50514