Theorem grplid 18998

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 18971	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpbn0.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grplid.p	. . 3 ⊢ + = (+g‘𝐺)
4		grplid.o	. . 3 ⊢ 0 = (0g‘𝐺)
5	2, 3, 4	mndlid 18780	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
6	1, 5	sylan 580	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  +_gcplusg 17298  0_gc0g 17486  Mndcmnd 18760  Grpcgrp 18964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fv 6571  df-riota 7388  df-ov 7434  df-0g 17488  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-grp 18967

This theorem is referenced by:  grplidd  19000  grprcan  19004  grpid  19006  isgrpid2  19007  grprinv  19021  grpinvid1  19022  grpinvid2  19023  grpidinv2  19028  grpinvid  19030  grplcan  19031  grpasscan1  19032  grpidlcan  19035  grplmulf1o  19044  grpidssd  19047  grpinvadd  19049  grpinvval2  19054  grplactcnv  19074  imasgrp  19087  mulgaddcom  19129  mulgdirlem  19136  subg0  19163  issubg2  19172  issubg4  19176  0subgOLD  19183  isnsg3  19191  nmzsubg  19196  ssnmz  19197  eqgid  19211  qusgrp  19217  qus0  19220  ghmid  19253  conjghm  19280  subgga  19331  cntzsubg  19370  sylow1lem2  19632  sylow2blem2  19654  sylow2blem3  19655  sylow3lem1  19660  lsmmod  19708  lsmdisj2  19715  pj1rid  19735  abladdsub4  19844  ablpncan2  19848  ablpnpcan  19852  ablnncan  19853  odadd1  19881  odadd2  19882  oddvdssubg  19888  dprdfadd  20055  pgpfac1lem3a  20111  rnglz  20183  rngrz  20184  isabvd  20830  lmod0vlid  20907  lmod0vs  20910  freshmansdream  21611  evpmodpmf1o  21632  ocvlss  21708  lsmcss  21728  psr0lid  21991  mplsubglem  22037  mplcoe1  22073  mdetunilem6  22639  mdetunilem9  22642  ghmcnp  24139  tgpt0  24143  qustgpopn  24144  mdegaddle  26128  ply1rem  26220  gsumsubg  33032  ogrpinv0le  33075  ogrpaddltrbid  33080  ogrpinv0lt  33082  ogrpinvlt  33083  cyc3genpmlem  33154  isarchi3  33177  archirngz  33179  archiabllem1b  33182  orngsqr  33314  ornglmulle  33315  orngrmulle  33316  qusker  33357  grplsm0l  33411  quslsm  33413  mxidlprm  33478  matunitlindflem1  37603  lfl0f  39051  lfladd0l  39056  lkrlss  39077  lkrin  39146  dvhgrp  41090  baerlem3lem1  41690  mapdh6bN  41720  hdmap1l6b  41794  hdmapinvlem3  41903  hdmapinvlem4  41904  hdmapglem7b  41911  fsuppind  42577  fsuppssind  42580