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

Theorem grplid 15727
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 15709 . 2
2 grpbn0.b . . 3
3 grplid.p . . 3
4 grplid.o . . 3
52, 3, 4mndlid 15600 . 2
61, 5sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  e.wcel 1758  `cfv 5537  (class class class)co 6222   cbs 14332   cplusg 14397   c0g 14537   cmnd 15568   cgrp 15569
This theorem is referenced by:  grprcan  15730  grpid  15732  isgrpid2  15733  grprinv  15744  grpinvid1  15745  grpinvid2  15746  grpinvid  15748  grplcan  15749  grpidlcan  15751  grplmulf1o  15759  grpidssd  15761  grpinvadd  15763  grpinvval2  15768  grplactcnv  15783  mulgdirlem  15810  imasgrp  15830  subg0  15846  issubg2  15855  issubg4  15859  0subg  15865  isnsg3  15874  nmzsubg  15881  ssnmz  15882  eqger  15890  eqgid  15892  divsgrp  15895  divs0  15898  ghmid  15912  conjghm  15936  conjnmz  15939  subgga  15977  cntzsubg  16013  sylow1lem2  16259  sylow2blem2  16281  sylow2blem3  16282  sylow3lem1  16287  lsmmod  16333  lsmdisj2  16340  pj1rid  16360  abladdsub4  16464  ablpncan2  16466  ablpnpcan  16470  ablnncan  16471  odadd1  16491  odadd2  16492  oddvdssubg  16498  dprdfadd  16685  dprdfaddOLD  16692  pgpfac1lem3a  16752  rnglz  16857  rngrz  16858  isabvd  17081  lmod0vlid  17154  lmod0vs  17157  psr0lid  17642  mplsubglem  17687  mplsubglemOLD  17689  mplcoe1  17721  evpmodpmf1o  18219  ocvlss  18290  lsmcss  18310  mdetunilem6  18691  mdetunilem9  18694  ghmcnp  20084  tgpt0  20088  divstgpopn  20089  mdegaddle  21945  ply1rem  22035  ogrpinvOLD  26639  ogrpinv0le  26640  ogrpaddltrbid  26645  ogrpinv0lt  26647  ogrpinvlt  26648  isarchi3  26665  archirngz  26667  archiabllem1b  26670  orngsqr  26729  ornglmulle  26730  orngrmulle  26731  ofldchr  26739  lfl0f  33565  lfladd0l  33570  lkrlss  33591  lkrin  33660  dvhgrp  35603  baerlem3lem1  36203  mapdh6bN  36233  hdmap1l6b  36308  hdmapinvlem3  36419  hdmapinvlem4  36420  hdmapglem7b  36427
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 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648
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 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3083  df-sbc 3298  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-mpt 4469  df-id 4753  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-iota 5500  df-fun 5539  df-fv 5545  df-riota 6183  df-ov 6225  df-0g 14539  df-mnd 15574  df-grp 15704
  Copyright terms: Public domain W3C validator