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

Theorem grplid 14790
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 14772 . 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 14671 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
61, 5sylan 458 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   ` cfv 5413  (class class class)co 6040   Basecbs 13424   +g cplusg 13484   0gc0g 13678   Mndcmnd 14639   Grpcgrp 14640
This theorem is referenced by:  grprcan  14793  grpid  14795  isgrpid2  14796  grprinv  14807  grpinvid1  14808  grpinvid2  14809  grpinvid  14811  grplcan  14812  grplmulf1o  14820  grpinvadd  14822  grpinvval2  14827  grplactcnv  14842  mulgdirlem  14869  imasgrp  14889  subg0  14905  issubg2  14914  issubg4  14916  0subg  14920  isnsg3  14929  nmzsubg  14936  ssnmz  14937  eqger  14945  eqgid  14947  divsgrp  14950  divs0  14953  ghmid  14967  conjghm  14991  conjnmz  14994  subgga  15032  cntzsubg  15090  sylow1lem2  15188  sylow2blem2  15210  sylow2blem3  15211  sylow3lem1  15216  lsmmod  15262  lsmdisj2  15269  pj1rid  15289  abladdsub4  15393  ablpncan2  15395  ablpnpcan  15399  ablnncan  15400  odadd1  15418  odadd2  15419  oddvdssubg  15425  dprdfadd  15533  pgpfac1lem3a  15589  rnglz  15655  rngrz  15656  isabvd  15863  lmod0vlid  15935  lmod0vs  15938  psr0lid  16414  mplsubglem  16453  mplcoe1  16483  ocvlss  16854  lsmcss  16874  ghmcnp  18097  tgpt0  18101  divstgpopn  18102  mdegaddle  19950  ply1rem  20039  ofldsqr  24193  ofldchr  24197  lfl0f  29552  lfladd0l  29557  lkrlss  29578  lkrin  29647  dvhgrp  31590  baerlem3lem1  32190  mapdh6bN  32220  hdmap1l6b  32295  hdmapinvlem3  32406  hdmapinvlem4  32407  hdmapglem7b  32414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-ov 6043  df-riota 6508  df-0g 13682  df-mnd 14645  df-grp 14767
  Copyright terms: Public domain W3C validator