Theorem mndidcl 18658

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  Basecbs 17155  +_gcplusg 17196  0_gc0g 17378  Mndcmnd 18643

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 5246  ax-nul 5256  ax-pr 5382

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 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-riota 7326  df-ov 7372  df-0g 17380  df-mgm 18549  df-sgrp 18628  df-mnd 18644

This theorem is referenced by:  mndbn0  18659  hashfinmndnn  18660  mndpfo  18666  mndpsuppss  18674  prdsidlem  18678  imasmnd  18684  xpsmnd0  18687  idmhm  18704  mhmf1o  18705  mndvlid  18708  mndvrid  18709  issubmd  18715  submid  18719  0subm  18726  0mhm  18728  mhmco  18732  mhmeql  18735  submacs  18736  mndind  18737  prdspjmhm  18738  pwsdiagmhm  18740  pwsco1mhm  18741  pwsco2mhm  18742  gsumvallem2  18743  dfgrp2  18876  grpidcl  18879  mhmid  18977  mhmmnd  18978  mulgnn0cl  19004  mulgnn0z  19015  cntzsubm  19252  oppgmnd  19268  gex1  19505  mulgnn0di  19739  mulgmhm  19741  subcmn  19751  gsumval3  19821  gsumzcl2  19824  gsumzaddlem  19835  gsumzsplit  19841  gsumzmhm  19851  gsummpt1n0  19879  simpgnideld  20015  submomnd  20046  omndmul2  20047  omndmul3  20048  omndmul  20049  ogrpinv0le  20050  gsumle  20059  srgidcl  20119  srg0cl  20120  ringidcl  20185  gsummgp0  20238  c0mgm  20379  c0mhm  20380  c0snmgmhm  20382  c0snmhm  20383  pwssplit1  20998  rngqiprngimf1  21242  dsmm0cl  21682  dsmmacl  21683  mhmcompl  22300  mdet0  22526  mndifsplit  22556  gsummatr01lem3  22577  pmatcollpw3fi1lem1  22706  tmdmulg  24012  tmdgsum  24015  tsms0  24062  tsmssplit  24072  tsmsxp  24075  mndlactfo  33011  mndractfo  33013  mndlactf1o  33014  mndractf1o  33015  gsumwun  33048  cntzsnid  33052  fxpsubm  33144  slmd0vcl  33190  ply1degltdimlem  33611  lvecendof1f1o  33622  sibf0  34318  sitmcl  34335  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  evl1gprodd  42098  ringexp0nn  42115  aks6d1c5lem2  42119  pwssplit4  43071  mgpsumz  48343  lco0  48409  mndtccatid  49569