Theorem mndidcl 18725

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6530  Basecbs 17226  +_gcplusg 17269  0_gc0g 17451  Mndcmnd 18710

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538  df-riota 7360  df-ov 7406  df-0g 17453  df-mgm 18616  df-sgrp 18695  df-mnd 18711

This theorem is referenced by:  mndbn0  18726  hashfinmndnn  18727  mndpfo  18733  mndpsuppss  18741  prdsidlem  18745  imasmnd  18751  xpsmnd0  18754  idmhm  18771  mhmf1o  18772  mndvlid  18775  mndvrid  18776  issubmd  18782  submid  18786  0subm  18793  0mhm  18795  mhmco  18799  mhmeql  18802  submacs  18803  mndind  18804  prdspjmhm  18805  pwsdiagmhm  18807  pwsco1mhm  18808  pwsco2mhm  18809  gsumvallem2  18810  dfgrp2  18943  grpidcl  18946  mhmid  19044  mhmmnd  19045  mulgnn0cl  19071  mulgnn0z  19082  cntzsubm  19319  oppgmnd  19335  gex1  19570  mulgnn0di  19804  mulgmhm  19806  subcmn  19816  gsumval3  19886  gsumzcl2  19889  gsumzaddlem  19900  gsumzsplit  19906  gsumzmhm  19916  gsummpt1n0  19944  simpgnideld  20080  srgidcl  20157  srg0cl  20158  ringidcl  20223  gsummgp0  20276  c0mgm  20417  c0mhm  20418  c0snmgmhm  20420  c0snmhm  20421  pwssplit1  21015  rngqiprngimf1  21259  dsmm0cl  21698  dsmmacl  21699  mhmcompl  22316  mdet0  22542  mndifsplit  22572  gsummatr01lem3  22593  pmatcollpw3fi1lem1  22722  tmdmulg  24028  tmdgsum  24031  tsms0  24078  tsmssplit  24088  tsmsxp  24091  mndlactfo  32968  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsumwun  33005  cntzsnid  33009  submomnd  33024  omndmul2  33026  omndmul3  33027  omndmul  33028  ogrpinv0le  33029  gsumle  33038  slmd0vcl  33164  ply1degltdimlem  33608  lvecendof1f1o  33619  sibf0  34312  sitmcl  34329  primrootsunit1  42056  primrootscoprmpow  42058  primrootscoprbij  42061  evl1gprodd  42076  ringexp0nn  42093  aks6d1c5lem2  42097  pwssplit4  43060  mgpsumz  48285  lco0  48351  mndtccatid  49412