MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mndidcl Structured version   Visualization version   GIF version

Theorem mndidcl 18576
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.
StepHypRef Expression
1 mndidcl.b . 2 𝐵 = (Base‘𝐺)
2 mndidcl.o . 2 0 = (0g𝐺)
3 eqid 2733 . 2 (+g𝐺) = (+g𝐺)
41, 3mndid 18571 . 2 (𝐺 ∈ Mnd → ∃𝑥𝐵𝑦𝐵 ((𝑥(+g𝐺)𝑦) = 𝑦 ∧ (𝑦(+g𝐺)𝑥) = 𝑦))
51, 2, 3, 4mgmidcl 18526 1 (𝐺 ∈ Mnd → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cfv 6497  Basecbs 17088  +gcplusg 17138  0gc0g 17326  Mndcmnd 18561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-iota 6449  df-fun 6499  df-fv 6505  df-riota 7314  df-ov 7361  df-0g 17328  df-mgm 18502  df-sgrp 18551  df-mnd 18562
This theorem is referenced by:  mndbn0  18577  hashfinmndnn  18578  mndpfo  18584  prdsidlem  18593  imasmnd  18599  idmhm  18616  mhmf1o  18617  issubmd  18622  submid  18626  0subm  18633  0mhm  18635  mhmco  18639  mhmeql  18641  submacs  18642  mndind  18643  prdspjmhm  18644  pwsdiagmhm  18646  pwsco1mhm  18647  pwsco2mhm  18648  gsumvallem2  18649  dfgrp2  18780  grpidcl  18783  mhmid  18873  mhmmnd  18874  mulgnn0cl  18897  mulgnn0z  18908  cntzsubm  19121  oppgmnd  19140  gex1  19378  mulgnn0di  19609  mulgmhm  19611  subcmn  19620  gsumval3  19689  gsumzcl2  19692  gsumzaddlem  19703  gsumzsplit  19709  gsumzmhm  19719  gsummpt1n0  19747  simpgnideld  19883  srgidcl  19935  srg0cl  19936  ringidcl  19994  gsummgp0  20037  pwssplit1  20535  dsmm0cl  21162  dsmmacl  21163  mndvlid  21758  mndvrid  21759  mdet0  21971  mndifsplit  22001  gsummatr01lem3  22022  pmatcollpw3fi1lem1  22151  tmdmulg  23459  tmdgsum  23462  tsms0  23509  tsmssplit  23519  tsmsxp  23522  cntzsnid  31952  submomnd  31967  omndmul2  31969  omndmul3  31970  omndmul  31971  ogrpinv0le  31972  gsumle  31981  slmd0vcl  32105  ply1degltdimlem  32374  sibf0  32991  sitmcl  33008  mhmcompl  40779  pwssplit4  41459  c0mgm  46293  c0mhm  46294  c0snmgmhm  46298  c0snmhm  46299  mgpsumz  46524  mndpsuppss  46533  lco0  46594  mndtccatid  47199
  Copyright terms: Public domain W3C validator