Theorem mndidcl 18623

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6482  Basecbs 17120  +_gcplusg 17161  0_gc0g 17343  Mndcmnd 18608

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 5235  ax-nul 5245  ax-pr 5371

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 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-riota 7306  df-ov 7352  df-0g 17345  df-mgm 18514  df-sgrp 18593  df-mnd 18609

This theorem is referenced by:  mndbn0  18624  hashfinmndnn  18625  mndpfo  18631  mndpsuppss  18639  prdsidlem  18643  imasmnd  18649  xpsmnd0  18652  idmhm  18669  mhmf1o  18670  mndvlid  18673  mndvrid  18674  issubmd  18680  submid  18684  0subm  18691  0mhm  18693  mhmco  18697  mhmeql  18700  submacs  18701  mndind  18702  prdspjmhm  18703  pwsdiagmhm  18705  pwsco1mhm  18706  pwsco2mhm  18707  gsumvallem2  18708  dfgrp2  18841  grpidcl  18844  mhmid  18942  mhmmnd  18943  mulgnn0cl  18969  mulgnn0z  18980  cntzsubm  19217  oppgmnd  19233  gex1  19470  mulgnn0di  19704  mulgmhm  19706  subcmn  19716  gsumval3  19786  gsumzcl2  19789  gsumzaddlem  19800  gsumzsplit  19806  gsumzmhm  19816  gsummpt1n0  19844  simpgnideld  19980  submomnd  20011  omndmul2  20012  omndmul3  20013  omndmul  20014  ogrpinv0le  20015  gsumle  20024  srgidcl  20084  srg0cl  20085  ringidcl  20150  gsummgp0  20203  c0mgm  20344  c0mhm  20345  c0snmgmhm  20347  c0snmhm  20348  pwssplit1  20963  rngqiprngimf1  21207  dsmm0cl  21647  dsmmacl  21648  mhmcompl  22265  mdet0  22491  mndifsplit  22521  gsummatr01lem3  22542  pmatcollpw3fi1lem1  22671  tmdmulg  23977  tmdgsum  23980  tsms0  24027  tsmssplit  24037  tsmsxp  24040  mndlactfo  32981  mndractfo  32983  mndlactf1o  32984  mndractf1o  32985  gsumwun  33018  cntzsnid  33022  fxpsubm  33114  slmd0vcl  33163  ply1degltdimlem  33589  lvecendof1f1o  33600  sibf0  34302  sitmcl  34319  primrootsunit1  42070  primrootscoprmpow  42072  primrootscoprbij  42075  evl1gprodd  42090  ringexp0nn  42107  aks6d1c5lem2  42111  pwssplit4  43062  mgpsumz  48346  lco0  48412  mndtccatid  49572