Theorem mndidcl 18802

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  Basecbs 17264  +_gcplusg 17305  0_gc0g 17487  Mndcmnd 18787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-riota 7367  df-ov 7413  df-0g 17489  df-mgm 18693  df-sgrp 18772  df-mnd 18788

This theorem is referenced by:  mndbn0  18803  hashfinmndnn  18804  mndpfo  18810  mndpsuppss  18818  prdsidlem  18822  imasmnd  18828  xpsmnd0  18831  idmhm  18848  mhmf1o  18849  mndvlid  18852  mndvrid  18853  issubmd  18859  submid  18863  0subm  18871  0mhm  18873  mhmco  18877  mhmeql  18880  submacs  18881  mndind  18882  prdspjmhm  18883  pwsdiagmhm  18885  pwsco1mhm  18886  pwsco2mhm  18887  gsumvallem2  18888  dfgrp2  19024  grpidcl  19027  mhmid  19124  mhmmnd  19125  mulgnn0cl  19151  mulgnn0z  19162  cntzsubm  19403  oppgmnd  19419  gex1  19656  mulgnn0di  19890  mulgmhm  19892  subcmn  19902  gsumval3  19972  gsumzcl2  19975  gsumzaddlem  19986  gsumzsplit  19992  gsumzmhm  20002  gsummpt1n0  20030  simpgnideld  20166  submomnd  20197  omndmul2  20198  omndmul3  20199  omndmul  20200  ogrpinv0le  20201  gsumle  20210  srgidcl  20276  srg0cl  20277  ringidcl  20344  gsummgp0  20395  c0mgm  20537  c0mhm  20538  c0snmgmhm  20540  c0snmhm  20541  pwssplit1  21180  rngqiprngimf1  21440  dsmm0cl  21890  dsmmacl  21891  mhmcompl  22272  mdet0  22763  mndifsplit  22793  gsummatr01lem3  22814  pmatcollpw3fi1lem1  22943  tmdmulg  24249  tmdgsum  24252  tsms0  24299  tsmssplit  24309  tsmsxp  24312  mndlactfo  33347  mndractfo  33349  mndlactf1o  33350  mndractf1o  33351  suppgsumssiun  33392  gsumwun  33396  cntzsnid  33400  fxpsubm  33492  slmd0vcl  33541  ply1degltdimlem  34012  lvecendof1f1o  34023  sibf0  34724  sitmcl  34741  primrootsunit1  42864  primrootscoprmpow  42866  primrootscoprbij  42869  evl1gprodd  42884  ringexp0nn  42901  aks6d1c5lem2  42905  pwssplit4  43816  mgpsumz  49142  lco0  49207  mndtccatid  50365