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

Theorem mndlid 18581
Description: The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
Hypotheses
Ref Expression
mndlrid.b 𝐵 = (Base‘𝐺)
mndlrid.p + = (+g𝐺)
mndlrid.o 0 = (0g𝐺)
Assertion
Ref Expression
mndlid ((𝐺 ∈ Mnd ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)

Proof of Theorem mndlid
StepHypRef Expression
1 mndlrid.b . . 3 𝐵 = (Base‘𝐺)
2 mndlrid.p . . 3 + = (+g𝐺)
3 mndlrid.o . . 3 0 = (0g𝐺)
41, 2, 3mndlrid 18580 . 2 ((𝐺 ∈ Mnd ∧ 𝑋𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
54simpld 496 1 ((𝐺 ∈ Mnd ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  cfv 6497  (class class class)co 7358  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:  issubmnd  18588  ress0g  18589  submnd0  18590  mndinvmod  18591  prdsidlem  18593  imasmnd  18599  0subm  18633  0mhm  18635  mndind  18643  gsumccat  18656  dfgrp2  18780  grplid  18785  dfgrp3  18851  mhmid  18873  mhmmnd  18874  mulgnn0p1  18892  mulgnn0z  18908  mulgnn0dir  18911  cntzsubm  19121  oppgmnd  19140  odmodnn0  19327  lsmub2x  19434  mulgnn0di  19609  gsumval3  19689  gsumzaddlem  19703  gsumzsplit  19709  srgbinomlem4  19965  dsmmacl  21163  mndvlid  21758  dmatmul  21862  mndifsplit  22001  tsmssplit  23519  cntzsnid  31952  omndmul2  31969  omndmul3  31970  slmd0vlid  32106  c0mgm  46293  c0mhm  46294  c0snmgmhm  46298  cznrng  46339  mndpsuppss  46533  mndtccatid  47199
  Copyright terms: Public domain W3C validator