Theorem grplid 18955

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ‘cfv 6544  (class class class)co 7414  Basecbs 17206  +_gcplusg 17259  0_gc0g 17447  Mndcmnd 18720  Grpcgrp 18921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3465  df-sbc 3777  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4324  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-br 5145  df-opab 5207  df-mpt 5228  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-iota 6496  df-fun 6546  df-fv 6552  df-riota 7370  df-ov 7417  df-0g 17449  df-mgm 18626  df-sgrp 18705  df-mnd 18721  df-grp 18924

This theorem is referenced by:  grplidd  18957  grprcan  18961  grpid  18963  isgrpid2  18964  grprinv  18978  grpinvid1  18979  grpinvid2  18980  grpidinv2  18985  grpinvid  18987  grplcan  18988  grpasscan1  18989  grpidlcan  18992  grplmulf1o  19001  grpidssd  19004  grpinvadd  19006  grpinvval2  19011  grplactcnv  19031  imasgrp  19044  mulgaddcom  19086  mulgdirlem  19093  subg0  19120  issubg2  19129  issubg4  19133  0subgOLD  19140  isnsg3  19148  nmzsubg  19153  ssnmz  19154  eqgid  19168  qusgrp  19174  qus0  19177  ghmid  19210  conjghm  19237  subgga  19288  cntzsubg  19327  sylow1lem2  19591  sylow2blem2  19613  sylow2blem3  19614  sylow3lem1  19619  lsmmod  19667  lsmdisj2  19674  pj1rid  19694  abladdsub4  19803  ablpncan2  19807  ablpnpcan  19811  ablnncan  19812  odadd1  19840  odadd2  19841  oddvdssubg  19847  dprdfadd  20014  pgpfac1lem3a  20070  rnglz  20142  rngrz  20143  isabvd  20785  lmod0vlid  20862  lmod0vs  20865  freshmansdream  21566  evpmodpmf1o  21586  ocvlss  21662  lsmcss  21682  psr0lid  21956  mplsubglem  22002  mplcoe1  22038  mhpaddcl  22139  mdetunilem6  22605  mdetunilem9  22608  ghmcnp  24105  tgpt0  24109  qustgpopn  24110  mdegaddle  26096  ply1rem  26188  gsumsubg  32916  ogrpinv0le  32952  ogrpaddltrbid  32957  ogrpinv0lt  32959  ogrpinvlt  32960  cyc3genpmlem  33031  isarchi3  33054  archirngz  33056  archiabllem1b  33059  orngsqr  33185  ornglmulle  33186  orngrmulle  33187  qusker  33228  grplsm0l  33282  quslsm  33284  mxidlprm  33349  matunitlindflem1  37328  lfl0f  38778  lfladd0l  38783  lkrlss  38804  lkrin  38873  dvhgrp  40817  baerlem3lem1  41417  mapdh6bN  41447  hdmap1l6b  41521  hdmapinvlem3  41630  hdmapinvlem4  41631  hdmapglem7b  41638  fsuppind  42278  fsuppssind  42281