Theorem grplid 19007

Description: The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)

Hypotheses

Ref	Expression
grpbn0.b	⊢ 𝐵 = (Base‘𝐺)
grplid.p	⊢ + = (+g‘𝐺)
grplid.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
grplid	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)

Proof of Theorem grplid

Step	Hyp	Ref	Expression
1		grpmnd 18980	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpbn0.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grplid.p	. . 3 ⊢ + = (+g‘𝐺)
4		grplid.o	. . 3 ⊢ 0 = (0g‘𝐺)
5	2, 3, 4	mndlid 18792	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
6	1, 5	sylan 579	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  0_gc0g 17499  Mndcmnd 18772  Grpcgrp 18973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-riota 7404  df-ov 7451  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976

This theorem is referenced by:  grplidd  19009  grprcan  19013  grpid  19015  isgrpid2  19016  grprinv  19030  grpinvid1  19031  grpinvid2  19032  grpidinv2  19037  grpinvid  19039  grplcan  19040  grpasscan1  19041  grpidlcan  19044  grplmulf1o  19053  grpidssd  19056  grpinvadd  19058  grpinvval2  19063  grplactcnv  19083  imasgrp  19096  mulgaddcom  19138  mulgdirlem  19145  subg0  19172  issubg2  19181  issubg4  19185  0subgOLD  19192  isnsg3  19200  nmzsubg  19205  ssnmz  19206  eqgid  19220  qusgrp  19226  qus0  19229  ghmid  19262  conjghm  19289  subgga  19340  cntzsubg  19379  sylow1lem2  19641  sylow2blem2  19663  sylow2blem3  19664  sylow3lem1  19669  lsmmod  19717  lsmdisj2  19724  pj1rid  19744  abladdsub4  19853  ablpncan2  19857  ablpnpcan  19861  ablnncan  19862  odadd1  19890  odadd2  19891  oddvdssubg  19897  dprdfadd  20064  pgpfac1lem3a  20120  rnglz  20192  rngrz  20193  isabvd  20835  lmod0vlid  20912  lmod0vs  20915  freshmansdream  21616  evpmodpmf1o  21637  ocvlss  21713  lsmcss  21733  psr0lid  21996  mplsubglem  22042  mplcoe1  22078  mdetunilem6  22644  mdetunilem9  22647  ghmcnp  24144  tgpt0  24148  qustgpopn  24149  mdegaddle  26133  ply1rem  26225  gsumsubg  33029  ogrpinv0le  33065  ogrpaddltrbid  33070  ogrpinv0lt  33072  ogrpinvlt  33073  cyc3genpmlem  33144  isarchi3  33167  archirngz  33169  archiabllem1b  33172  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  qusker  33342  grplsm0l  33396  quslsm  33398  mxidlprm  33463  matunitlindflem1  37576  lfl0f  39025  lfladd0l  39030  lkrlss  39051  lkrin  39120  dvhgrp  41064  baerlem3lem1  41664  mapdh6bN  41694  hdmap1l6b  41768  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem7b  41885  fsuppind  42545  fsuppssind  42548