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

Theorem grplid 15559
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 15541 . 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 15433 . 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 1369    e. wcel 1756   ` cfv 5413  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   0gc0g 14370   Mndcmnd 15401   Grpcgrp 15402
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 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526
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 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421  df-riota 6047  df-ov 6089  df-0g 14372  df-mnd 15407  df-grp 15536
This theorem is referenced by:  grprcan  15562  grpid  15564  isgrpid2  15565  grprinv  15576  grpinvid1  15577  grpinvid2  15578  grpinvid  15580  grplcan  15581  grpidlcan  15583  grplmulf1o  15591  grpidssd  15593  grpinvadd  15595  grpinvval2  15600  grplactcnv  15615  mulgdirlem  15642  imasgrp  15662  subg0  15678  issubg2  15687  issubg4  15691  0subg  15697  isnsg3  15706  nmzsubg  15713  ssnmz  15714  eqger  15722  eqgid  15724  divsgrp  15727  divs0  15730  ghmid  15744  conjghm  15768  conjnmz  15771  subgga  15809  cntzsubg  15845  sylow1lem2  16089  sylow2blem2  16111  sylow2blem3  16112  sylow3lem1  16117  lsmmod  16163  lsmdisj2  16170  pj1rid  16190  abladdsub4  16294  ablpncan2  16296  ablpnpcan  16300  ablnncan  16301  odadd1  16321  odadd2  16322  oddvdssubg  16328  dprdfadd  16500  dprdfaddOLD  16507  pgpfac1lem3a  16567  rnglz  16671  rngrz  16672  isabvd  16885  lmod0vlid  16958  lmod0vs  16961  psr0lid  17446  mplsubglem  17490  mplsubglemOLD  17492  mplcoe1  17524  evpmodpmf1o  18006  ocvlss  18077  lsmcss  18097  mdetunilem6  18403  mdetunilem9  18406  ghmcnp  19665  tgpt0  19669  divstgpopn  19670  mdegaddle  21525  ply1rem  21615  ogrpinvOLD  26146  ogrpinv0le  26147  ogrpaddltrbid  26152  ogrpinv0lt  26154  ogrpinvlt  26155  isarchi3  26172  archirngz  26174  archiabllem1b  26177  orngsqr  26240  ornglmulle  26241  orngrmulle  26242  ofldchr  26250  lfl0f  32607  lfladd0l  32612  lkrlss  32633  lkrin  32702  dvhgrp  34645  baerlem3lem1  35245  mapdh6bN  35275  hdmap1l6b  35350  hdmapinvlem3  35461  hdmapinvlem4  35462  hdmapglem7b  35469
  Copyright terms: Public domain W3C validator