Theorem mndidcl 18674

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  Basecbs 17136  +_gcplusg 17177  0_gc0g 17359  Mndcmnd 18659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7315  df-ov 7361  df-0g 17361  df-mgm 18565  df-sgrp 18644  df-mnd 18660

This theorem is referenced by:  mndbn0  18675  hashfinmndnn  18676  mndpfo  18682  mndpsuppss  18690  prdsidlem  18694  imasmnd  18700  xpsmnd0  18703  idmhm  18720  mhmf1o  18721  mndvlid  18724  mndvrid  18725  issubmd  18731  submid  18735  0subm  18742  0mhm  18744  mhmco  18748  mhmeql  18751  submacs  18752  mndind  18753  prdspjmhm  18754  pwsdiagmhm  18756  pwsco1mhm  18757  pwsco2mhm  18758  gsumvallem2  18759  dfgrp2  18892  grpidcl  18895  mhmid  18993  mhmmnd  18994  mulgnn0cl  19020  mulgnn0z  19031  cntzsubm  19267  oppgmnd  19283  gex1  19520  mulgnn0di  19754  mulgmhm  19756  subcmn  19766  gsumval3  19836  gsumzcl2  19839  gsumzaddlem  19850  gsumzsplit  19856  gsumzmhm  19866  gsummpt1n0  19894  simpgnideld  20030  submomnd  20061  omndmul2  20062  omndmul3  20063  omndmul  20064  ogrpinv0le  20065  gsumle  20074  srgidcl  20134  srg0cl  20135  ringidcl  20200  gsummgp0  20253  c0mgm  20395  c0mhm  20396  c0snmgmhm  20398  c0snmhm  20399  pwssplit1  21011  rngqiprngimf1  21255  dsmm0cl  21695  dsmmacl  21696  mhmcompl  22324  mdet0  22550  mndifsplit  22580  gsummatr01lem3  22601  pmatcollpw3fi1lem1  22730  tmdmulg  24036  tmdgsum  24039  tsms0  24086  tsmssplit  24096  tsmsxp  24099  mndlactfo  33109  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  gsumwun  33158  cntzsnid  33162  fxpsubm  33254  slmd0vcl  33303  ply1degltdimlem  33779  lvecendof1f1o  33790  sibf0  34491  sitmcl  34508  primrootsunit1  42351  primrootscoprmpow  42353  primrootscoprbij  42356  evl1gprodd  42371  ringexp0nn  42388  aks6d1c5lem2  42392  pwssplit4  43331  mgpsumz  48608  lco0  48673  mndtccatid  49832