Theorem mndidcl 18652

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

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

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 18543  df-sgrp 18622  df-mnd 18638

This theorem is referenced by:  mndbn0  18653  hashfinmndnn  18654  mndpfo  18660  mndpsuppss  18668  prdsidlem  18672  imasmnd  18678  xpsmnd0  18681  idmhm  18698  mhmf1o  18699  mndvlid  18702  mndvrid  18703  issubmd  18709  submid  18713  0subm  18720  0mhm  18722  mhmco  18726  mhmeql  18729  submacs  18730  mndind  18731  prdspjmhm  18732  pwsdiagmhm  18734  pwsco1mhm  18735  pwsco2mhm  18736  gsumvallem2  18737  dfgrp2  18870  grpidcl  18873  mhmid  18971  mhmmnd  18972  mulgnn0cl  18998  mulgnn0z  19009  cntzsubm  19246  oppgmnd  19262  gex1  19497  mulgnn0di  19731  mulgmhm  19733  subcmn  19743  gsumval3  19813  gsumzcl2  19816  gsumzaddlem  19827  gsumzsplit  19833  gsumzmhm  19843  gsummpt1n0  19871  simpgnideld  20007  srgidcl  20084  srg0cl  20085  ringidcl  20150  gsummgp0  20203  c0mgm  20344  c0mhm  20345  c0snmgmhm  20347  c0snmhm  20348  pwssplit1  20942  rngqiprngimf1  21186  dsmm0cl  21625  dsmmacl  21626  mhmcompl  22243  mdet0  22469  mndifsplit  22499  gsummatr01lem3  22520  pmatcollpw3fi1lem1  22649  tmdmulg  23955  tmdgsum  23958  tsms0  24005  tsmssplit  24015  tsmsxp  24018  mndlactfo  32941  mndractfo  32943  mndlactf1o  32944  mndractf1o  32945  gsumwun  32978  cntzsnid  32982  submomnd  32997  omndmul2  32999  omndmul3  33000  omndmul  33001  ogrpinv0le  33002  gsumle  33011  fxpsubm  33102  slmd0vcl  33147  ply1degltdimlem  33591  lvecendof1f1o  33602  sibf0  34298  sitmcl  34315  primrootsunit1  42058  primrootscoprmpow  42060  primrootscoprbij  42063  evl1gprodd  42078  ringexp0nn  42095  aks6d1c5lem2  42099  pwssplit4  43051  mgpsumz  48323  lco0  48389  mndtccatid  49549