Theorem mndidcl 18649

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  ‘cfv 6477  Basecbs 17112  +_gcplusg 17153  0_gc0g 17335  Mndcmnd 18634

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3344  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6433  df-fun 6479  df-fv 6485  df-riota 7298  df-ov 7344  df-0g 17337  df-mgm 18540  df-sgrp 18619  df-mnd 18635

This theorem is referenced by:  mndbn0  18650  hashfinmndnn  18651  mndpfo  18657  mndpsuppss  18665  prdsidlem  18669  imasmnd  18675  xpsmnd0  18678  idmhm  18695  mhmf1o  18696  mndvlid  18699  mndvrid  18700  issubmd  18706  submid  18710  0subm  18717  0mhm  18719  mhmco  18723  mhmeql  18726  submacs  18727  mndind  18728  prdspjmhm  18729  pwsdiagmhm  18731  pwsco1mhm  18732  pwsco2mhm  18733  gsumvallem2  18734  dfgrp2  18867  grpidcl  18870  mhmid  18968  mhmmnd  18969  mulgnn0cl  18995  mulgnn0z  19006  cntzsubm  19243  oppgmnd  19259  gex1  19496  mulgnn0di  19730  mulgmhm  19732  subcmn  19742  gsumval3  19812  gsumzcl2  19815  gsumzaddlem  19826  gsumzsplit  19832  gsumzmhm  19842  gsummpt1n0  19870  simpgnideld  20006  submomnd  20037  omndmul2  20038  omndmul3  20039  omndmul  20040  ogrpinv0le  20041  gsumle  20050  srgidcl  20110  srg0cl  20111  ringidcl  20176  gsummgp0  20229  c0mgm  20370  c0mhm  20371  c0snmgmhm  20373  c0snmhm  20374  pwssplit1  20986  rngqiprngimf1  21230  dsmm0cl  21670  dsmmacl  21671  mhmcompl  22288  mdet0  22514  mndifsplit  22544  gsummatr01lem3  22565  pmatcollpw3fi1lem1  22694  tmdmulg  24000  tmdgsum  24003  tsms0  24050  tsmssplit  24060  tsmsxp  24063  mndlactfo  32998  mndractfo  33000  mndlactf1o  33001  mndractf1o  33002  gsumwun  33035  cntzsnid  33039  fxpsubm  33131  slmd0vcl  33180  ply1degltdimlem  33625  lvecendof1f1o  33636  sibf0  34337  sitmcl  34354  primrootsunit1  42109  primrootscoprmpow  42111  primrootscoprbij  42114  evl1gprodd  42129  ringexp0nn  42146  aks6d1c5lem2  42150  pwssplit4  43101  mgpsumz  48372  lco0  48438  mndtccatid  49598