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

Theorem mndlid 15460
Description: The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
Hypotheses
Ref Expression
mndlrid.b  |-  B  =  ( Base `  G
)
mndlrid.p  |-  .+  =  ( +g  `  G )
mndlrid.o  |-  .0.  =  ( 0g `  G )
Assertion
Ref Expression
mndlid  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )

Proof of Theorem mndlid
StepHypRef Expression
1 mndlrid.b . . 3  |-  B  =  ( Base `  G
)
2 mndlrid.p . . 3  |-  .+  =  ( +g  `  G )
3 mndlrid.o . . 3  |-  .0.  =  ( 0g `  G )
41, 2, 3mndlrid 15459 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  ( (  .0.  .+  X )  =  X  /\  ( X  .+  .0.  )  =  X
) )
54simpld 459 1  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   ` cfv 5437  (class class class)co 6110   Basecbs 14193   +g cplusg 14257   0gc0g 14397   Mndcmnd 15428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-reu 2741  df-rmo 2742  df-rab 2743  df-v 2993  df-sbc 3206  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-br 4312  df-opab 4370  df-mpt 4371  df-id 4655  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-iota 5400  df-fun 5439  df-fv 5445  df-riota 6071  df-ov 6113  df-0g 14399  df-mnd 15434
This theorem is referenced by:  issubmnd  15468  ress0g  15469  submnd0  15470  prdsidlem  15472  imasmnd  15478  0mhm  15505  mrcmndind  15513  gsumccat  15538  grplid  15587  mulgnn0p1  15657  mulgnn0z  15666  mulgnn0dir  15669  cntzsubm  15872  oppgmnd  15888  odmodnn0  16062  lsmub2x  16165  mulgnn0di  16332  gsumval3OLD  16401  gsumval3  16404  gsumzaddlem  16427  gsumzaddlemOLD  16429  gsumzsplit  16437  gsumzsplitOLD  16438  srgbinomlem4  16660  dsmmacl  18185  mndvlid  18312  mndifsplit  18461  tsmssplit  19745  omndmul2  26194  omndmul3  26195  slmd0vlid  26257  mndpsuppss  30807  dmatmul  30899
  Copyright terms: Public domain W3C validator