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

Theorem grplid 15548
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 15530 . 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 15424 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
61, 5sylan 468 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755   ` cfv 5406  (class class class)co 6080   Basecbs 14157   +g cplusg 14221   0gc0g 14361   Mndcmnd 15392   Grpcgrp 15393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fv 5414  df-riota 6039  df-ov 6083  df-0g 14363  df-mnd 15398  df-grp 15525
This theorem is referenced by:  grprcan  15551  grpid  15553  isgrpid2  15554  grprinv  15565  grpinvid1  15566  grpinvid2  15567  grpinvid  15569  grplcan  15570  grpidlcan  15572  grplmulf1o  15580  grpidssd  15582  grpinvadd  15584  grpinvval2  15589  grplactcnv  15604  mulgdirlem  15631  imasgrp  15651  subg0  15667  issubg2  15676  issubg4  15680  0subg  15686  isnsg3  15695  nmzsubg  15702  ssnmz  15703  eqger  15711  eqgid  15713  divsgrp  15716  divs0  15719  ghmid  15733  conjghm  15757  conjnmz  15760  subgga  15798  cntzsubg  15834  sylow1lem2  16078  sylow2blem2  16100  sylow2blem3  16101  sylow3lem1  16106  lsmmod  16152  lsmdisj2  16159  pj1rid  16179  abladdsub4  16283  ablpncan2  16285  ablpnpcan  16289  ablnncan  16290  odadd1  16310  odadd2  16311  oddvdssubg  16317  dprdfadd  16484  dprdfaddOLD  16491  pgpfac1lem3a  16551  rnglz  16617  rngrz  16618  isabvd  16829  lmod0vlid  16902  lmod0vs  16905  psr0lid  17400  mplsubglem  17444  mplsubglemOLD  17446  mplcoe1  17478  evpmodpmf1o  17868  ocvlss  17939  lsmcss  17959  mdetunilem6  18265  mdetunilem9  18268  ghmcnp  19527  tgpt0  19531  divstgpopn  19532  mdegaddle  21430  ply1rem  21520  ogrpinvOLD  26002  ogrpinv0le  26003  ogrpaddltrbid  26008  ogrpinv0lt  26010  ogrpinvlt  26011  isarchi3  26028  archirngz  26030  archiabllem1b  26033  orngsqr  26125  ornglmulle  26126  orngrmulle  26127  ofldchr  26135  lfl0f  32308  lfladd0l  32313  lkrlss  32334  lkrin  32403  dvhgrp  34346  baerlem3lem1  34946  mapdh6bN  34976  hdmap1l6b  35051  hdmapinvlem3  35162  hdmapinvlem4  35163  hdmapglem7b  35170
  Copyright terms: Public domain W3C validator