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

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

Proof of Theorem grplid
StepHypRef Expression
1 grpmnd 16666 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpbn0.b . . 3  |-  B  =  ( Base `  G
)
3 grplid.p . . 3  |-  .+  =  ( +g  `  G )
4 grplid.o . . 3  |-  .0.  =  ( 0g `  G )
52, 3, 4mndlid 16545 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
61, 5sylan 473 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   ` cfv 5598  (class class class)co 6302   Basecbs 15109   +g cplusg 15178   0gc0g 15326   Mndcmnd 16523   Grpcgrp 16657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-iota 5562  df-fun 5600  df-fv 5606  df-riota 6264  df-ov 6305  df-0g 15328  df-mgm 16476  df-sgrp 16515  df-mnd 16525  df-grp 16661
This theorem is referenced by:  grprcan  16687  grpid  16689  isgrpid2  16690  grprinv  16701  grpinvid1  16702  grpinvid2  16703  grpinvid  16705  grplcan  16706  grpidlcan  16708  grplmulf1o  16716  grpidssd  16718  grpinvadd  16720  grpinvval2  16725  grplactcnv  16742  mulgdirlem  16770  imasgrp  16790  subg0  16811  issubg2  16820  issubg4  16824  0subg  16830  isnsg3  16839  nmzsubg  16846  ssnmz  16847  eqger  16855  eqgid  16857  qusgrp  16860  qus0  16863  ghmid  16877  conjghm  16901  conjnmz  16904  subgga  16942  cntzsubg  16978  sylow1lem2  17239  sylow2blem2  17261  sylow2blem3  17262  sylow3lem1  17267  lsmmod  17313  lsmdisj2  17320  pj1rid  17340  abladdsub4  17444  ablpncan2  17446  ablpnpcan  17450  ablnncan  17451  odadd1  17474  odadd2  17475  oddvdssubg  17481  dprdfadd  17641  pgpfac1lem3a  17697  ringlz  17805  ringrz  17806  isabvd  18036  lmod0vlid  18109  lmod0vs  18112  psr0lid  18607  mplsubglem  18646  mplcoe1  18677  evpmodpmf1o  19151  ocvlss  19222  lsmcss  19242  mdetunilem6  19629  mdetunilem9  19632  ghmcnp  21116  tgpt0  21120  qustgpopn  21121  mdegaddle  23010  ply1rem  23101  ogrpinvOLD  28473  ogrpinv0le  28474  ogrpaddltrbid  28479  ogrpinv0lt  28481  ogrpinvlt  28482  isarchi3  28499  archirngz  28501  archiabllem1b  28504  orngsqr  28563  ornglmulle  28564  orngrmulle  28565  ofldchr  28573  lfl0f  32554  lfladd0l  32559  lkrlss  32580  lkrin  32649  dvhgrp  34594  baerlem3lem1  35194  mapdh6bN  35224  hdmap1l6b  35299  hdmapinvlem3  35410  hdmapinvlem4  35411  hdmapglem7b  35418  rnglz  39156
  Copyright terms: Public domain W3C validator