Theorem grplid 18985

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  0_gc0g 17484  Mndcmnd 18747  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-riota 7388  df-ov 7434  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954

This theorem is referenced by:  grplidd  18987  grprcan  18991  grpid  18993  isgrpid2  18994  grprinv  19008  grpinvid1  19009  grpinvid2  19010  grpidinv2  19015  grpinvid  19017  grplcan  19018  grpasscan1  19019  grpidlcan  19022  grplmulf1o  19031  grpidssd  19034  grpinvadd  19036  grpinvval2  19041  grplactcnv  19061  imasgrp  19074  mulgaddcom  19116  mulgdirlem  19123  subg0  19150  issubg2  19159  issubg4  19163  0subgOLD  19170  isnsg3  19178  nmzsubg  19183  ssnmz  19184  eqgid  19198  qusgrp  19204  qus0  19207  ghmid  19240  conjghm  19267  subgga  19318  cntzsubg  19357  sylow1lem2  19617  sylow2blem2  19639  sylow2blem3  19640  sylow3lem1  19645  lsmmod  19693  lsmdisj2  19700  pj1rid  19720  abladdsub4  19829  ablpncan2  19833  ablpnpcan  19837  ablnncan  19838  odadd1  19866  odadd2  19867  oddvdssubg  19873  dprdfadd  20040  pgpfac1lem3a  20096  rnglz  20162  rngrz  20163  isabvd  20813  lmod0vlid  20890  lmod0vs  20893  freshmansdream  21593  evpmodpmf1o  21614  ocvlss  21690  lsmcss  21710  psr0lid  21973  mplsubglem  22019  mplcoe1  22055  mdetunilem6  22623  mdetunilem9  22626  ghmcnp  24123  tgpt0  24127  qustgpopn  24128  mdegaddle  26113  ply1rem  26205  gsumsubg  33049  ogrpinv0le  33092  ogrpaddltrbid  33097  ogrpinv0lt  33099  ogrpinvlt  33100  cyc3genpmlem  33171  isarchi3  33194  archirngz  33196  archiabllem1b  33199  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  qusker  33377  grplsm0l  33431  quslsm  33433  mxidlprm  33498  matunitlindflem1  37623  lfl0f  39070  lfladd0l  39075  lkrlss  39096  lkrin  39165  dvhgrp  41109  baerlem3lem1  41709  mapdh6bN  41739  hdmap1l6b  41813  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem7b  41930  fsuppind  42600  fsuppssind  42603