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

Theorem grplid 15505
Description: The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
Hypotheses
Ref Expression
grpbn0.b
grplid.p
grplid.o
Assertion
Ref Expression
grplid

Proof of Theorem grplid
StepHypRef Expression
1 grpmnd 15487 . 2
2 grpbn0.b . . 3
3 grplid.p . . 3
4 grplid.o . . 3
52, 3, 4mndlid 15381 . 2
61, 5sylan 461 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  =wceq 1687  e.wcel 1749  `cfv 5390  (class class class)co 6061   cbs 14114   cplusg 14178   c0g 14318   cmnd 15349   cgrp 15350
This theorem is referenced by:  grprcan  15508  grpid  15510  isgrpid2  15511  grprinv  15522  grpinvid1  15523  grpinvid2  15524  grpinvid  15526  grplcan  15527  grpidlcan  15529  grplmulf1o  15537  grpidssd  15539  grpinvadd  15541  grpinvval2  15546  grplactcnv  15561  mulgdirlem  15588  imasgrp  15608  subg0  15624  issubg2  15633  issubg4  15637  0subg  15643  isnsg3  15652  nmzsubg  15659  ssnmz  15660  eqger  15668  eqgid  15670  divsgrp  15673  divs0  15676  ghmid  15690  conjghm  15714  conjnmz  15717  subgga  15755  cntzsubg  15791  sylow1lem2  16035  sylow2blem2  16057  sylow2blem3  16058  sylow3lem1  16063  lsmmod  16109  lsmdisj2  16116  pj1rid  16136  abladdsub4  16240  ablpncan2  16242  ablpnpcan  16246  ablnncan  16247  odadd1  16266  odadd2  16267  oddvdssubg  16273  dprdfadd  16387  pgpfac1lem3a  16443  rnglz  16509  rngrz  16510  isabvd  16718  lmod0vlid  16791  lmod0vs  16794  psr0lid  17279  mplsubglem  17321  mplcoe1  17351  evpmodpmf1o  17734  ocvlss  17805  lsmcss  17825  mdetunilem6  18125  mdetunilem9  18128  ghmcnp  19389  tgpt0  19393  divstgpopn  19394  mdegaddle  21287  ply1rem  21376  ogrpinvOLD  25857  ogrpinv0le  25858  ogrpaddltrbid  25863  ogrpinv0lt  25865  ogrpinvlt  25866  isarchi3  25883  archirngz  25885  archiabllem1b  25888  orngsqr  25980  ornglmulle  25981  orngrmulle  25982  ofldchr  25990  lfl0f  32151  lfladd0l  32156  lkrlss  32177  lkrin  32246  dvhgrp  34189  baerlem3lem1  34789  mapdh6bN  34819  hdmap1l6b  34894  hdmapinvlem3  35005  hdmapinvlem4  35006  hdmapglem7b  35013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-opab 4326  df-mpt 4327  df-id 4607  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-iota 5353  df-fun 5392  df-fv 5398  df-riota 6020  df-ov 6064  df-0g 14320  df-mnd 15355  df-grp 15482
  Copyright terms: Public domain W3C validator