Theorem mndidcl 18810

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2150  ‘cfv 6540  Basecbs 17272  +_gcplusg 17313  0_gc0g 17495  Mndcmnd 18795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-nul 5274  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ne 2966  df-ral 3087  df-rex 3097  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3464  df-sbc 3753  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 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5560  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-iota 6496  df-fun 6542  df-fv 6548  df-riota 7371  df-ov 7417  df-0g 17497  df-mgm 18701  df-sgrp 18780  df-mnd 18796

This theorem is referenced by:  mndbn0  18811  hashfinmndnn  18812  mndpfo  18818  mndpsuppss  18826  prdsidlem  18830  imasmnd  18836  xpsmnd0  18839  idmhm  18856  mhmf1o  18857  mndvlid  18860  mndvrid  18861  issubmd  18867  submid  18871  0subm  18879  0mhm  18881  mhmco  18885  mhmeql  18888  submacs  18889  mndind  18890  prdspjmhm  18891  pwsdiagmhm  18893  pwsco1mhm  18894  pwsco2mhm  18895  gsumvallem2  18896  dfgrp2  19032  grpidcl  19035  mhmid  19132  mhmmnd  19133  mulgnn0cl  19159  mulgnn0z  19170  cntzsubm  19411  oppgmnd  19427  gex1  19664  mulgnn0di  19898  mulgmhm  19900  subcmn  19910  gsumval3  19980  gsumzcl2  19983  gsumzaddlem  19994  gsumzsplit  20000  gsumzmhm  20010  gsummpt1n0  20038  simpgnideld  20174  submomnd  20205  omndmul2  20206  omndmul3  20207  omndmul  20208  ogrpinv0le  20209  gsumle  20218  srgidcl  20284  srg0cl  20285  ringidcl  20351  gsummgp0  20402  c0mgm  20544  c0mhm  20545  c0snmgmhm  20547  c0snmhm  20548  pwssplit1  21163  rngqiprngimf1  21423  dsmm0cl  21873  dsmmacl  21874  mhmcompl  22255  mdet0  22746  mndifsplit  22776  gsummatr01lem3  22797  pmatcollpw3fi1lem1  22926  tmdmulg  24232  tmdgsum  24235  tsms0  24282  tsmssplit  24292  tsmsxp  24295  mndlactfo  33317  mndractfo  33319  mndlactf1o  33320  mndractf1o  33321  suppgsumssiun  33362  gsumwun  33366  cntzsnid  33370  fxpsubm  33462  slmd0vcl  33511  ply1degltdimlem  33982  lvecendof1f1o  33993  sibf0  34694  sitmcl  34711  primrootsunit1  42814  primrootscoprmpow  42816  primrootscoprbij  42819  evl1gprodd  42834  ringexp0nn  42851  aks6d1c5lem2  42855  pwssplit4  43768  mgpsumz  49091  lco0  49156  mndtccatid  50314