Theorem grplid 18909

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  0_gc0g 17371  Mndcmnd 18671  Grpcgrp 18875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-riota 7325  df-ov 7371  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878

This theorem is referenced by:  grplidd  18911  grprcan  18915  grpid  18917  isgrpid2  18918  grprinv  18932  grpinvid1  18933  grpinvid2  18934  grpidinv2  18939  grpinvid  18941  grplcan  18942  grpasscan1  18943  grpidlcan  18946  grplmulf1o  18955  grpidssd  18958  grpinvadd  18960  grpinvval2  18965  grplactcnv  18985  imasgrp  18998  mulgaddcom  19040  mulgdirlem  19047  subg0  19074  issubg2  19083  issubg4  19087  isnsg3  19101  nmzsubg  19106  ssnmz  19107  eqgid  19121  qusgrp  19127  qus0  19130  ghmid  19163  conjghm  19190  subgga  19241  cntzsubg  19280  sylow1lem2  19540  sylow2blem2  19562  sylow2blem3  19563  sylow3lem1  19568  lsmmod  19616  lsmdisj2  19623  pj1rid  19643  abladdsub4  19752  ablpncan2  19756  ablpnpcan  19760  ablnncan  19761  odadd1  19789  odadd2  19790  oddvdssubg  19796  dprdfadd  19963  pgpfac1lem3a  20019  ogrpinv0le  20077  ogrpaddltrbid  20082  ogrpinv0lt  20084  ogrpinvlt  20085  rnglz  20112  rngrz  20113  isabvd  20757  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  lmod0vlid  20855  lmod0vs  20858  freshmansdream  21541  evpmodpmf1o  21563  ocvlss  21639  lsmcss  21659  psr0lid  21921  mplsubglem  21966  mplcoe1  22004  mdetunilem6  22573  mdetunilem9  22576  ghmcnp  24071  tgpt0  24075  qustgpopn  24076  mdegaddle  26047  ply1rem  26139  gsumsubg  33139  cyc3genpmlem  33244  isarchi3  33280  archirngz  33282  archiabllem1b  33285  qusker  33441  grplsm0l  33495  quslsm  33497  mxidlprm  33562  matunitlindflem1  37861  lfl0f  39439  lfladd0l  39444  lkrlss  39465  lkrin  39534  dvhgrp  41477  baerlem3lem1  42077  mapdh6bN  42107  hdmap1l6b  42181  hdmapinvlem3  42290  hdmapinvlem4  42291  hdmapglem7b  42298  fsuppind  42942  fsuppssind  42945