Theorem mndidcl 18787

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  Basecbs 17258  +_gcplusg 17311  0_gc0g 17499  Mndcmnd 18772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-riota 7404  df-ov 7451  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773

This theorem is referenced by:  mndbn0  18788  hashfinmndnn  18789  mndpfo  18795  prdsidlem  18804  imasmnd  18810  xpsmnd0  18813  idmhm  18830  mhmf1o  18831  mndvlid  18834  mndvrid  18835  issubmd  18841  submid  18845  0subm  18852  0mhm  18854  mhmco  18858  mhmeql  18861  submacs  18862  mndind  18863  prdspjmhm  18864  pwsdiagmhm  18866  pwsco1mhm  18867  pwsco2mhm  18868  gsumvallem2  18869  dfgrp2  19002  grpidcl  19005  mhmid  19103  mhmmnd  19104  mulgnn0cl  19130  mulgnn0z  19141  cntzsubm  19378  oppgmnd  19397  gex1  19633  mulgnn0di  19867  mulgmhm  19869  subcmn  19879  gsumval3  19949  gsumzcl2  19952  gsumzaddlem  19963  gsumzsplit  19969  gsumzmhm  19979  gsummpt1n0  20007  simpgnideld  20143  srgidcl  20226  srg0cl  20227  ringidcl  20289  gsummgp0  20341  c0mgm  20485  c0mhm  20486  c0snmgmhm  20488  c0snmhm  20489  pwssplit1  21081  rngqiprngimf1  21333  dsmm0cl  21783  dsmmacl  21784  mhmcompl  22405  mdet0  22633  mndifsplit  22663  gsummatr01lem3  22684  pmatcollpw3fi1lem1  22813  tmdmulg  24121  tmdgsum  24124  tsms0  24171  tsmssplit  24181  tsmsxp  24184  mndlactfo  33013  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  cntzsnid  33045  submomnd  33060  omndmul2  33062  omndmul3  33063  omndmul  33064  ogrpinv0le  33065  gsumle  33074  slmd0vcl  33200  ply1degltdimlem  33635  lvecendof1f1o  33646  sibf0  34299  sitmcl  34316  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  evl1gprodd  42074  ringexp0nn  42091  aks6d1c5lem2  42095  pwssplit4  43046  mgpsumz  48087  mndpsuppss  48096  lco0  48156  mndtccatid  48760