Theorem grplid 18136

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  +_gcplusg 16568  0_gc0g 16716  Mndcmnd 17914  Grpcgrp 18106

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-iota 6317  df-fun 6360  df-fv 6366  df-riota 7117  df-ov 7162  df-0g 16718  df-mgm 17855  df-sgrp 17904  df-mnd 17915  df-grp 18109

This theorem is referenced by:  grprcan  18140  grpid  18142  isgrpid2  18143  grprinv  18156  grpinvid1  18157  grpinvid2  18158  grpidinv2  18161  grpinvid  18163  grplcan  18164  grpasscan1  18165  grpidlcan  18168  grplmulf1o  18176  grpidssd  18178  grpinvadd  18180  grpinvval2  18185  grplactcnv  18205  imasgrp  18218  mulgaddcom  18254  mulgdirlem  18261  subg0  18288  issubg2  18297  issubg4  18301  0subg  18307  isnsg3  18315  nmzsubg  18320  ssnmz  18321  eqger  18333  eqgid  18335  qusgrp  18338  qus0  18341  ghmid  18367  conjghm  18392  conjnmz  18395  subgga  18433  cntzsubg  18470  sylow1lem2  18727  sylow2blem2  18749  sylow2blem3  18750  sylow3lem1  18755  lsmmod  18804  lsmdisj2  18811  pj1rid  18831  abladdsub4  18937  ablpncan2  18939  ablpnpcan  18943  ablnncan  18944  odadd1  18971  odadd2  18972  oddvdssubg  18978  dprdfadd  19145  pgpfac1lem3a  19201  ringlz  19340  ringrz  19341  isabvd  19594  lmod0vlid  19667  lmod0vs  19670  psr0lid  20178  mplsubglem  20217  mplcoe1  20249  mhpaddcl  20341  evpmodpmf1o  20743  ocvlss  20819  lsmcss  20839  mdetunilem6  21229  mdetunilem9  21232  ghmcnp  22726  tgpt0  22730  qustgpopn  22731  mdegaddle  24671  ply1rem  24760  gsumsubg  30688  ogrpinv0le  30720  ogrpaddltrbid  30725  ogrpinv0lt  30727  ogrpinvlt  30728  cyc3genpmlem  30797  isarchi3  30820  archirngz  30822  archiabllem1b  30825  freshmansdream  30863  orngsqr  30881  ornglmulle  30882  orngrmulle  30883  ofldchr  30891  qusker  30922  mxidlprm  30981  dimkerim  31027  matunitlindflem1  34892  lfl0f  36209  lfladd0l  36214  lkrlss  36235  lkrin  36304  dvhgrp  38247  baerlem3lem1  38847  mapdh6bN  38877  hdmap1l6b  38951  hdmapinvlem3  39060  hdmapinvlem4  39061  hdmapglem7b  39068  rnglz  44162