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

Theorem grplid 15874
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 15856 . 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 15747 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
61, 5sylan 471 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  (  .0.  .+  X
)  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   ` cfv 5579  (class class class)co 6275   Basecbs 14479   +g cplusg 14544   0gc0g 14684   Mndcmnd 15715   Grpcgrp 15716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fv 5587  df-riota 6236  df-ov 6278  df-0g 14686  df-mnd 15721  df-grp 15851
This theorem is referenced by:  grprcan  15877  grpid  15879  isgrpid2  15880  grprinv  15891  grpinvid1  15892  grpinvid2  15893  grpinvid  15895  grplcan  15896  grpidlcan  15898  grplmulf1o  15906  grpidssd  15908  grpinvadd  15910  grpinvval2  15915  grplactcnv  15932  mulgdirlem  15959  imasgrp  15979  subg0  15995  issubg2  16004  issubg4  16008  0subg  16014  isnsg3  16023  nmzsubg  16030  ssnmz  16031  eqger  16039  eqgid  16041  divsgrp  16044  divs0  16047  ghmid  16061  conjghm  16085  conjnmz  16088  subgga  16126  cntzsubg  16162  sylow1lem2  16408  sylow2blem2  16430  sylow2blem3  16431  sylow3lem1  16436  lsmmod  16482  lsmdisj2  16489  pj1rid  16509  abladdsub4  16613  ablpncan2  16615  ablpnpcan  16619  ablnncan  16620  odadd1  16640  odadd2  16641  oddvdssubg  16647  dprdfadd  16843  dprdfaddOLD  16850  pgpfac1lem3a  16910  rnglz  17015  rngrz  17016  isabvd  17245  lmod0vlid  17318  lmod0vs  17321  psr0lid  17812  mplsubglem  17857  mplsubglemOLD  17859  mplcoe1  17891  evpmodpmf1o  18392  ocvlss  18463  lsmcss  18483  mdetunilem6  18879  mdetunilem9  18882  ghmcnp  20341  tgpt0  20345  divstgpopn  20346  mdegaddle  22202  ply1rem  22292  ogrpinvOLD  27217  ogrpinv0le  27218  ogrpaddltrbid  27223  ogrpinv0lt  27225  ogrpinvlt  27226  isarchi3  27243  archirngz  27245  archiabllem1b  27248  orngsqr  27307  ornglmulle  27308  orngrmulle  27309  ofldchr  27317  lfl0f  33741  lfladd0l  33746  lkrlss  33767  lkrin  33836  dvhgrp  35779  baerlem3lem1  36379  mapdh6bN  36409  hdmap1l6b  36484  hdmapinvlem3  36595  hdmapinvlem4  36596  hdmapglem7b  36603
  Copyright terms: Public domain W3C validator