Theorem mndidcl 18783

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  Basecbs 17245  +_gcplusg 17286  0_gc0g 17468  Mndcmnd 18768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6477  df-fun 6523  df-fv 6529  df-riota 7353  df-ov 7399  df-0g 17470  df-mgm 18674  df-sgrp 18753  df-mnd 18769

This theorem is referenced by:  mndbn0  18784  hashfinmndnn  18785  mndpfo  18791  mndpsuppss  18799  prdsidlem  18803  imasmnd  18809  xpsmnd0  18812  idmhm  18829  mhmf1o  18830  mndvlid  18833  mndvrid  18834  issubmd  18840  submid  18844  0subm  18851  0mhm  18853  mhmco  18857  mhmeql  18860  submacs  18861  mndind  18862  prdspjmhm  18863  pwsdiagmhm  18865  pwsco1mhm  18866  pwsco2mhm  18867  gsumvallem2  18868  dfgrp2  19004  grpidcl  19007  mhmid  19105  mhmmnd  19106  mulgnn0cl  19132  mulgnn0z  19143  cntzsubm  19378  oppgmnd  19394  gex1  19631  mulgnn0di  19865  mulgmhm  19867  subcmn  19877  gsumval3  19947  gsumzcl2  19950  gsumzaddlem  19961  gsumzsplit  19967  gsumzmhm  19977  gsummpt1n0  20005  simpgnideld  20141  submomnd  20172  omndmul2  20173  omndmul3  20174  omndmul  20175  ogrpinv0le  20176  gsumle  20185  srgidcl  20245  srg0cl  20246  ringidcl  20311  gsummgp0  20362  c0mgm  20504  c0mhm  20505  c0snmgmhm  20507  c0snmhm  20508  pwssplit1  21123  rngqiprngimf1  21367  dsmm0cl  21789  dsmmacl  21790  mhmcompl  22171  mdet0  22663  mndifsplit  22693  gsummatr01lem3  22714  pmatcollpw3fi1lem1  22843  tmdmulg  24149  tmdgsum  24152  tsms0  24199  tsmssplit  24209  tsmsxp  24212  mndlactfo  33202  mndractfo  33204  mndlactf1o  33205  mndractf1o  33206  suppgsumssiun  33249  gsumwun  33253  cntzsnid  33257  fxpsubm  33349  slmd0vcl  33398  ply1degltdimlem  33916  lvecendof1f1o  33927  sibf0  34628  sitmcl  34645  primrootsunit1  42711  primrootscoprmpow  42713  primrootscoprbij  42716  evl1gprodd  42731  ringexp0nn  42748  aks6d1c5lem2  42752  pwssplit4  43663  mgpsumz  48981  lco0  49046  mndtccatid  50205