Theorem mndidcl 18708

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  Basecbs 17170  +_gcplusg 17211  0_gc0g 17393  Mndcmnd 18693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493  df-riota 7313  df-ov 7359  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694

This theorem is referenced by:  mndbn0  18709  hashfinmndnn  18710  mndpfo  18716  mndpsuppss  18724  prdsidlem  18728  imasmnd  18734  xpsmnd0  18737  idmhm  18754  mhmf1o  18755  mndvlid  18758  mndvrid  18759  issubmd  18765  submid  18769  0subm  18776  0mhm  18778  mhmco  18782  mhmeql  18785  submacs  18786  mndind  18787  prdspjmhm  18788  pwsdiagmhm  18790  pwsco1mhm  18791  pwsco2mhm  18792  gsumvallem2  18793  dfgrp2  18929  grpidcl  18932  mhmid  19030  mhmmnd  19031  mulgnn0cl  19057  mulgnn0z  19068  cntzsubm  19304  oppgmnd  19320  gex1  19557  mulgnn0di  19791  mulgmhm  19793  subcmn  19803  gsumval3  19873  gsumzcl2  19876  gsumzaddlem  19887  gsumzsplit  19893  gsumzmhm  19903  gsummpt1n0  19931  simpgnideld  20067  submomnd  20098  omndmul2  20099  omndmul3  20100  omndmul  20101  ogrpinv0le  20102  gsumle  20111  srgidcl  20171  srg0cl  20172  ringidcl  20237  gsummgp0  20288  c0mgm  20430  c0mhm  20431  c0snmgmhm  20433  c0snmhm  20434  pwssplit1  21049  rngqiprngimf1  21293  dsmm0cl  21715  dsmmacl  21716  mhmcompl  22097  mdet0  22589  mndifsplit  22619  gsummatr01lem3  22640  pmatcollpw3fi1lem1  22769  tmdmulg  24075  tmdgsum  24078  tsms0  24125  tsmssplit  24135  tsmsxp  24138  mndlactfo  33106  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  suppgsumssiun  33153  gsumwun  33157  cntzsnid  33161  fxpsubm  33253  slmd0vcl  33302  ply1degltdimlem  33806  lvecendof1f1o  33817  sibf0  34518  sitmcl  34535  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  evl1gprodd  42602  ringexp0nn  42619  aks6d1c5lem2  42623  pwssplit4  43534  mgpsumz  48853  lco0  48918  mndtccatid  50077