Theorem grplid 18897

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  0_gc0g 17359  Mndcmnd 18659  Grpcgrp 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7315  df-ov 7361  df-0g 17361  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18866

This theorem is referenced by:  grplidd  18899  grprcan  18903  grpid  18905  isgrpid2  18906  grprinv  18920  grpinvid1  18921  grpinvid2  18922  grpidinv2  18927  grpinvid  18929  grplcan  18930  grpasscan1  18931  grpidlcan  18934  grplmulf1o  18943  grpidssd  18946  grpinvadd  18948  grpinvval2  18953  grplactcnv  18973  imasgrp  18986  mulgaddcom  19028  mulgdirlem  19035  subg0  19062  issubg2  19071  issubg4  19075  isnsg3  19089  nmzsubg  19094  ssnmz  19095  eqgid  19109  qusgrp  19115  qus0  19118  ghmid  19151  conjghm  19178  subgga  19229  cntzsubg  19268  sylow1lem2  19528  sylow2blem2  19550  sylow2blem3  19551  sylow3lem1  19556  lsmmod  19604  lsmdisj2  19611  pj1rid  19631  abladdsub4  19740  ablpncan2  19744  ablpnpcan  19748  ablnncan  19749  odadd1  19777  odadd2  19778  oddvdssubg  19784  dprdfadd  19951  pgpfac1lem3a  20007  ogrpinv0le  20065  ogrpaddltrbid  20070  ogrpinv0lt  20072  ogrpinvlt  20073  rnglz  20100  rngrz  20101  isabvd  20745  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  lmod0vlid  20843  lmod0vs  20846  freshmansdream  21529  evpmodpmf1o  21551  ocvlss  21627  lsmcss  21647  psr0lid  21909  mplsubglem  21954  mplcoe1  21992  mdetunilem6  22561  mdetunilem9  22564  ghmcnp  24059  tgpt0  24063  qustgpopn  24064  mdegaddle  26035  ply1rem  26127  gsumsubg  33129  cyc3genpmlem  33233  isarchi3  33269  archirngz  33271  archiabllem1b  33274  qusker  33430  grplsm0l  33484  quslsm  33486  mxidlprm  33551  matunitlindflem1  37813  lfl0f  39325  lfladd0l  39330  lkrlss  39351  lkrin  39420  dvhgrp  41363  baerlem3lem1  41963  mapdh6bN  41993  hdmap1l6b  42067  hdmapinvlem3  42176  hdmapinvlem4  42177  hdmapglem7b  42184  fsuppind  42829  fsuppssind  42832