Theorem mndidcl 18672

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6490  Basecbs 17134  +_gcplusg 17175  0_gc0g 17357  Mndcmnd 18657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498  df-riota 7313  df-ov 7359  df-0g 17359  df-mgm 18563  df-sgrp 18642  df-mnd 18658

This theorem is referenced by:  mndbn0  18673  hashfinmndnn  18674  mndpfo  18680  mndpsuppss  18688  prdsidlem  18692  imasmnd  18698  xpsmnd0  18701  idmhm  18718  mhmf1o  18719  mndvlid  18722  mndvrid  18723  issubmd  18729  submid  18733  0subm  18740  0mhm  18742  mhmco  18746  mhmeql  18749  submacs  18750  mndind  18751  prdspjmhm  18752  pwsdiagmhm  18754  pwsco1mhm  18755  pwsco2mhm  18756  gsumvallem2  18757  dfgrp2  18890  grpidcl  18893  mhmid  18991  mhmmnd  18992  mulgnn0cl  19018  mulgnn0z  19029  cntzsubm  19265  oppgmnd  19281  gex1  19518  mulgnn0di  19752  mulgmhm  19754  subcmn  19764  gsumval3  19834  gsumzcl2  19837  gsumzaddlem  19848  gsumzsplit  19854  gsumzmhm  19864  gsummpt1n0  19892  simpgnideld  20028  submomnd  20059  omndmul2  20060  omndmul3  20061  omndmul  20062  ogrpinv0le  20063  gsumle  20072  srgidcl  20132  srg0cl  20133  ringidcl  20198  gsummgp0  20251  c0mgm  20393  c0mhm  20394  c0snmgmhm  20396  c0snmhm  20397  pwssplit1  21009  rngqiprngimf1  21253  dsmm0cl  21693  dsmmacl  21694  mhmcompl  22322  mdet0  22548  mndifsplit  22578  gsummatr01lem3  22599  pmatcollpw3fi1lem1  22728  tmdmulg  24034  tmdgsum  24037  tsms0  24084  tsmssplit  24094  tsmsxp  24097  mndlactfo  33058  mndractfo  33060  mndlactf1o  33061  mndractf1o  33062  gsumwun  33107  cntzsnid  33111  fxpsubm  33203  slmd0vcl  33252  ply1degltdimlem  33728  lvecendof1f1o  33739  sibf0  34440  sitmcl  34457  primrootsunit1  42290  primrootscoprmpow  42292  primrootscoprbij  42295  evl1gprodd  42310  ringexp0nn  42327  aks6d1c5lem2  42331  pwssplit4  43273  mgpsumz  48550  lco0  48615  mndtccatid  49774