Theorem grplid 18934

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  0_gc0g 17393  Mndcmnd 18693  Grpcgrp 18900

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 5231  ax-nul 5241  ax-pr 5370

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 7317  df-ov 7363  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903

This theorem is referenced by:  grplidd  18936  grprcan  18940  grpid  18942  isgrpid2  18943  grprinv  18957  grpinvid1  18958  grpinvid2  18959  grpidinv2  18964  grpinvid  18966  grplcan  18967  grpasscan1  18968  grpidlcan  18971  grplmulf1o  18980  grpidssd  18983  grpinvadd  18985  grpinvval2  18990  grplactcnv  19010  imasgrp  19023  mulgaddcom  19065  mulgdirlem  19072  subg0  19099  issubg2  19108  issubg4  19112  isnsg3  19126  nmzsubg  19131  ssnmz  19132  eqgid  19146  qusgrp  19152  qus0  19155  ghmid  19188  conjghm  19215  subgga  19266  cntzsubg  19305  sylow1lem2  19565  sylow2blem2  19587  sylow2blem3  19588  sylow3lem1  19593  lsmmod  19641  lsmdisj2  19648  pj1rid  19668  abladdsub4  19777  ablpncan2  19781  ablpnpcan  19785  ablnncan  19786  odadd1  19814  odadd2  19815  oddvdssubg  19821  dprdfadd  19988  pgpfac1lem3a  20044  ogrpinv0le  20102  ogrpaddltrbid  20107  ogrpinv0lt  20109  ogrpinvlt  20110  rnglz  20137  rngrz  20138  isabvd  20780  orngsqr  20834  ornglmulle  20835  orngrmulle  20836  lmod0vlid  20878  lmod0vs  20881  freshmansdream  21564  evpmodpmf1o  21586  ocvlss  21662  lsmcss  21682  psr0lid  21942  mplsubglem  21987  mplcoe1  22025  mdetunilem6  22592  mdetunilem9  22595  ghmcnp  24090  tgpt0  24094  qustgpopn  24095  mdegaddle  26049  ply1rem  26141  gsumsubg  33122  cyc3genpmlem  33227  isarchi3  33263  archirngz  33265  archiabllem1b  33268  qusker  33424  grplsm0l  33478  quslsm  33480  mxidlprm  33545  matunitlindflem1  37951  lfl0f  39529  lfladd0l  39534  lkrlss  39555  lkrin  39624  dvhgrp  41567  baerlem3lem1  42167  mapdh6bN  42197  hdmap1l6b  42271  hdmapinvlem3  42380  hdmapinvlem4  42381  hdmapglem7b  42388  fsuppind  43037  fsuppssind  43040