Theorem mndidcl 18683

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  Basecbs 17186  +_gcplusg 17227  0_gc0g 17409  Mndcmnd 18668

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-riota 7347  df-ov 7393  df-0g 17411  df-mgm 18574  df-sgrp 18653  df-mnd 18669

This theorem is referenced by:  mndbn0  18684  hashfinmndnn  18685  mndpfo  18691  mndpsuppss  18699  prdsidlem  18703  imasmnd  18709  xpsmnd0  18712  idmhm  18729  mhmf1o  18730  mndvlid  18733  mndvrid  18734  issubmd  18740  submid  18744  0subm  18751  0mhm  18753  mhmco  18757  mhmeql  18760  submacs  18761  mndind  18762  prdspjmhm  18763  pwsdiagmhm  18765  pwsco1mhm  18766  pwsco2mhm  18767  gsumvallem2  18768  dfgrp2  18901  grpidcl  18904  mhmid  19002  mhmmnd  19003  mulgnn0cl  19029  mulgnn0z  19040  cntzsubm  19277  oppgmnd  19293  gex1  19528  mulgnn0di  19762  mulgmhm  19764  subcmn  19774  gsumval3  19844  gsumzcl2  19847  gsumzaddlem  19858  gsumzsplit  19864  gsumzmhm  19874  gsummpt1n0  19902  simpgnideld  20038  srgidcl  20115  srg0cl  20116  ringidcl  20181  gsummgp0  20234  c0mgm  20375  c0mhm  20376  c0snmgmhm  20378  c0snmhm  20379  pwssplit1  20973  rngqiprngimf1  21217  dsmm0cl  21656  dsmmacl  21657  mhmcompl  22274  mdet0  22500  mndifsplit  22530  gsummatr01lem3  22551  pmatcollpw3fi1lem1  22680  tmdmulg  23986  tmdgsum  23989  tsms0  24036  tsmssplit  24046  tsmsxp  24049  mndlactfo  32975  mndractfo  32977  mndlactf1o  32978  mndractf1o  32979  gsumwun  33012  cntzsnid  33016  submomnd  33031  omndmul2  33033  omndmul3  33034  omndmul  33035  ogrpinv0le  33036  gsumle  33045  fxpsubm  33136  slmd0vcl  33181  ply1degltdimlem  33625  lvecendof1f1o  33636  sibf0  34332  sitmcl  34349  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  evl1gprodd  42112  ringexp0nn  42129  aks6d1c5lem2  42133  pwssplit4  43085  mgpsumz  48354  lco0  48420  mndtccatid  49580