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

Theorem grplid 15670
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 15652 . 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 15543 . 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 1370    e. wcel 1758   ` cfv 5516  (class class class)co 6190   Basecbs 14276   +g cplusg 14340   0gc0g 14480   Mndcmnd 15511   Grpcgrp 15512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fv 5524  df-riota 6151  df-ov 6193  df-0g 14482  df-mnd 15517  df-grp 15647
This theorem is referenced by:  grprcan  15673  grpid  15675  isgrpid2  15676  grprinv  15687  grpinvid1  15688  grpinvid2  15689  grpinvid  15691  grplcan  15692  grpidlcan  15694  grplmulf1o  15702  grpidssd  15704  grpinvadd  15706  grpinvval2  15711  grplactcnv  15726  mulgdirlem  15753  imasgrp  15773  subg0  15789  issubg2  15798  issubg4  15802  0subg  15808  isnsg3  15817  nmzsubg  15824  ssnmz  15825  eqger  15833  eqgid  15835  divsgrp  15838  divs0  15841  ghmid  15855  conjghm  15879  conjnmz  15882  subgga  15920  cntzsubg  15956  sylow1lem2  16202  sylow2blem2  16224  sylow2blem3  16225  sylow3lem1  16230  lsmmod  16276  lsmdisj2  16283  pj1rid  16303  abladdsub4  16407  ablpncan2  16409  ablpnpcan  16413  ablnncan  16414  odadd1  16434  odadd2  16435  oddvdssubg  16441  dprdfadd  16615  dprdfaddOLD  16622  pgpfac1lem3a  16682  rnglz  16787  rngrz  16788  isabvd  17011  lmod0vlid  17084  lmod0vs  17087  psr0lid  17572  mplsubglem  17617  mplsubglemOLD  17619  mplcoe1  17651  evpmodpmf1o  18135  ocvlss  18206  lsmcss  18226  mdetunilem6  18539  mdetunilem9  18542  ghmcnp  19801  tgpt0  19805  divstgpopn  19806  mdegaddle  21661  ply1rem  21751  ogrpinvOLD  26312  ogrpinv0le  26313  ogrpaddltrbid  26318  ogrpinv0lt  26320  ogrpinvlt  26321  isarchi3  26338  archirngz  26340  archiabllem1b  26343  orngsqr  26406  ornglmulle  26407  orngrmulle  26408  ofldchr  26416  lfl0f  33020  lfladd0l  33025  lkrlss  33046  lkrin  33115  dvhgrp  35058  baerlem3lem1  35658  mapdh6bN  35688  hdmap1l6b  35763  hdmapinvlem3  35874  hdmapinvlem4  35875  hdmapglem7b  35882
  Copyright terms: Public domain W3C validator