Theorem mndidcl 18676

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  Basecbs 17179  +_gcplusg 17220  0_gc0g 17402  Mndcmnd 18661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-riota 7344  df-ov 7390  df-0g 17404  df-mgm 18567  df-sgrp 18646  df-mnd 18662

This theorem is referenced by:  mndbn0  18677  hashfinmndnn  18678  mndpfo  18684  mndpsuppss  18692  prdsidlem  18696  imasmnd  18702  xpsmnd0  18705  idmhm  18722  mhmf1o  18723  mndvlid  18726  mndvrid  18727  issubmd  18733  submid  18737  0subm  18744  0mhm  18746  mhmco  18750  mhmeql  18753  submacs  18754  mndind  18755  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  gsumvallem2  18761  dfgrp2  18894  grpidcl  18897  mhmid  18995  mhmmnd  18996  mulgnn0cl  19022  mulgnn0z  19033  cntzsubm  19270  oppgmnd  19286  gex1  19521  mulgnn0di  19755  mulgmhm  19757  subcmn  19767  gsumval3  19837  gsumzcl2  19840  gsumzaddlem  19851  gsumzsplit  19857  gsumzmhm  19867  gsummpt1n0  19895  simpgnideld  20031  srgidcl  20108  srg0cl  20109  ringidcl  20174  gsummgp0  20227  c0mgm  20368  c0mhm  20369  c0snmgmhm  20371  c0snmhm  20372  pwssplit1  20966  rngqiprngimf1  21210  dsmm0cl  21649  dsmmacl  21650  mhmcompl  22267  mdet0  22493  mndifsplit  22523  gsummatr01lem3  22544  pmatcollpw3fi1lem1  22673  tmdmulg  23979  tmdgsum  23982  tsms0  24029  tsmssplit  24039  tsmsxp  24042  mndlactfo  32968  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsumwun  33005  cntzsnid  33009  submomnd  33024  omndmul2  33026  omndmul3  33027  omndmul  33028  ogrpinv0le  33029  gsumle  33038  fxpsubm  33129  slmd0vcl  33174  ply1degltdimlem  33618  lvecendof1f1o  33629  sibf0  34325  sitmcl  34342  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  evl1gprodd  42105  ringexp0nn  42122  aks6d1c5lem2  42126  pwssplit4  43078  mgpsumz  48350  lco0  48416  mndtccatid  49576