Theorem mndidcl 18674

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6543  Basecbs 17148  +_gcplusg 17201  0_gc0g 17389  Mndcmnd 18659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-riota 7367  df-ov 7414  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660

This theorem is referenced by:  mndbn0  18675  hashfinmndnn  18676  mndpfo  18682  prdsidlem  18691  imasmnd  18697  xpsmnd0  18700  idmhm  18717  mhmf1o  18718  issubmd  18723  submid  18727  0subm  18734  0mhm  18736  mhmco  18740  mhmeql  18743  submacs  18744  mndind  18745  prdspjmhm  18746  pwsdiagmhm  18748  pwsco1mhm  18749  pwsco2mhm  18750  gsumvallem2  18751  dfgrp2  18883  grpidcl  18886  mhmid  18982  mhmmnd  18983  mulgnn0cl  19006  mulgnn0z  19017  cntzsubm  19243  oppgmnd  19262  gex1  19500  mulgnn0di  19734  mulgmhm  19736  subcmn  19746  gsumval3  19816  gsumzcl2  19819  gsumzaddlem  19830  gsumzsplit  19836  gsumzmhm  19846  gsummpt1n0  19874  simpgnideld  20010  srgidcl  20093  srg0cl  20094  ringidcl  20154  gsummgp0  20206  c0mgm  20350  c0mhm  20351  c0snmgmhm  20353  c0snmhm  20354  pwssplit1  20814  rngqiprngimf1  21059  dsmm0cl  21514  dsmmacl  21515  mndvlid  22115  mndvrid  22116  mdet0  22328  mndifsplit  22358  gsummatr01lem3  22379  pmatcollpw3fi1lem1  22508  tmdmulg  23816  tmdgsum  23819  tsms0  23866  tsmssplit  23876  tsmsxp  23879  cntzsnid  32471  submomnd  32486  omndmul2  32488  omndmul3  32489  omndmul  32490  ogrpinv0le  32491  gsumle  32500  slmd0vcl  32624  ply1degltdimlem  32983  sibf0  33619  sitmcl  33636  mhmcompl  41422  pwssplit4  42133  mgpsumz  47127  mndpsuppss  47136  lco0  47196  mndtccatid  47801