Theorem mndidcl 18989

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6566  Basecbs 17431  +_gcplusg 17472  0_gc0g 17660  Mndcmnd 18973

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574  df-riota 7408  df-ov 7454  df-0g 17662  df-mgm 18866  df-sgrp 18958  df-mnd 18974

This theorem is used by:  mndbn0  18990  hashfinmndnn  18991  mndpfoOLD  18999  mndpsuppss  19009  prdsidlem  19013  imasmnd  19019  xpsmnd0  19022  idmhm  19040  mhmf1o  19041  mndvlid  19044  mndvrid  19045  issubmd  19051  submid  19055  0subm  19063  0mhm  19065  mhmco  19069  mhmeql  19072  submacs  19073  mndind  19074  prdspjmhm  19075  pwsdiagmhm  19077  pwsco1mhm  19078  pwsco2mhm  19079  gsumvallem2  19080  dfgrp2  19223  grpidcl  19226  mhmid  19323  mhmmnd  19324  mulgnn0cl  19350  mulgnn0z  19361  cntzsubm  19603  oppgmnd  19619  gex1  19856  mulgnn0di  20090  mulgmhm  20092  subcmn  20102  gsumval3  20172  gsumzcl2  20175  gsumzaddlem  20186  gsumzsplit  20192  gsumzmhm  20202  gsummpt1n0  20230  simpgnideld  20366  submomnd  20397  omndmul2  20398  omndmul3  20399  omndmul  20400  ogrpinv0le  20401  gsumle  20410  srgidcl  20476  srg0cl  20477  ringidcl  20545  gsummgp0  20598  c0mgm  20740  c0mhm  20741  c0snmgmhm  20743  c0snmhm  20744  pwssplit1  21385  rngqiprngimf1  21647  dsmm0cl  22101  dsmmacl  22102  mhmcompl  22485  mdet0  22976  mndifsplit  23006  gsummatr01lem3  23027  pmatcollpw3fi1lem1  23159  tmdmulg  24466  tmdgsum  24469  tsms0  24516  tsmssplit  24526  tsmsxp  24529  mndlactfo  33687  mndractfo  33689  mndlactf1o  33690  mndractf1o  33691  suppgsumssiun  33732  gsumwun  33736  cntzsnid  33740  fxpsubm  33832  slmd0vcl  33881  ply1degltdimlem  34365  lvecendof1f1o  34376  sibf0  35077  sitmcl  35094  primrootsunit1  43413  primrootscoprmpow  43415  primrootscoprbij  43418  evl1gprodd  43433  ringexp0nn  43450  aks6d1c5lem2  43454  pwssplit4  44357  mgpsumz  49805  lco0  49870  mndtccatid  51056