Theorem mndidcl 18806

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  Basecbs 17268  +_gcplusg 17309  0_gc0g 17491  Mndcmnd 18791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-riota 7368  df-ov 7414  df-0g 17493  df-mgm 18697  df-sgrp 18776  df-mnd 18792

This theorem is referenced by:  mndbn0  18807  hashfinmndnn  18808  mndpfo  18814  mndpsuppss  18822  prdsidlem  18826  imasmnd  18832  xpsmnd0  18835  idmhm  18852  mhmf1o  18853  mndvlid  18856  mndvrid  18857  issubmd  18863  submid  18867  0subm  18875  0mhm  18877  mhmco  18881  mhmeql  18884  submacs  18885  mndind  18886  prdspjmhm  18887  pwsdiagmhm  18889  pwsco1mhm  18890  pwsco2mhm  18891  gsumvallem2  18892  dfgrp2  19028  grpidcl  19031  mhmid  19128  mhmmnd  19129  mulgnn0cl  19155  mulgnn0z  19166  cntzsubm  19407  oppgmnd  19423  gex1  19660  mulgnn0di  19894  mulgmhm  19896  subcmn  19906  gsumval3  19976  gsumzcl2  19979  gsumzaddlem  19990  gsumzsplit  19996  gsumzmhm  20006  gsummpt1n0  20034  simpgnideld  20170  submomnd  20201  omndmul2  20202  omndmul3  20203  omndmul  20204  ogrpinv0le  20205  gsumle  20214  srgidcl  20280  srg0cl  20281  ringidcl  20347  gsummgp0  20398  c0mgm  20540  c0mhm  20541  c0snmgmhm  20543  c0snmhm  20544  pwssplit1  21157  rngqiprngimf1  21410  dsmm0cl  21858  dsmmacl  21859  mhmcompl  22240  mdet0  22731  mndifsplit  22761  gsummatr01lem3  22782  pmatcollpw3fi1lem1  22911  tmdmulg  24217  tmdgsum  24220  tsms0  24267  tsmssplit  24277  tsmsxp  24280  mndlactfo  33287  mndractfo  33289  mndlactf1o  33290  mndractf1o  33291  suppgsumssiun  33332  gsumwun  33336  cntzsnid  33340  fxpsubm  33432  slmd0vcl  33481  ply1degltdimlem  33956  lvecendof1f1o  33967  sibf0  34668  sitmcl  34685  primrootsunit1  42753  primrootscoprmpow  42755  primrootscoprbij  42758  evl1gprodd  42773  ringexp0nn  42790  aks6d1c5lem2  42794  pwssplit4  43707  mgpsumz  49026  lco0  49091  mndtccatid  50249