Theorem grplid 18888

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 18862	. 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 396   = wceq 1541   ∈ wcel 2106  ‘cfv 6543  (class class class)co 7411  Basecbs 17148  +_gcplusg 17201  0_gc0g 17389  Mndcmnd 18659  Grpcgrp 18855

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-riota 7367  df-ov 7414  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858

This theorem is referenced by:  grplidd  18890  grprcan  18894  grpid  18896  isgrpid2  18897  grprinv  18911  grpinvid1  18912  grpinvid2  18913  grpidinv2  18918  grpinvid  18920  grplcan  18921  grpasscan1  18922  grpidlcan  18925  grplmulf1o  18933  grpidssd  18935  grpinvadd  18937  grpinvval2  18942  grplactcnv  18962  imasgrp  18975  mulgaddcom  19014  mulgdirlem  19021  subg0  19048  issubg2  19057  issubg4  19061  0subgOLD  19068  isnsg3  19076  nmzsubg  19081  ssnmz  19082  eqgid  19096  qusgrp  19101  qus0  19104  ghmid  19136  conjghm  19163  conjnmz  19166  subgga  19205  cntzsubg  19244  sylow1lem2  19508  sylow2blem2  19530  sylow2blem3  19531  sylow3lem1  19536  lsmmod  19584  lsmdisj2  19591  pj1rid  19611  abladdsub4  19720  ablpncan2  19724  ablpnpcan  19728  ablnncan  19729  odadd1  19757  odadd2  19758  oddvdssubg  19764  dprdfadd  19931  pgpfac1lem3a  19987  rnglz  20059  rngrz  20060  isabvd  20571  lmod0vlid  20646  lmod0vs  20649  evpmodpmf1o  21368  ocvlss  21444  lsmcss  21464  psr0lid  21733  mplsubglem  21777  mplcoe1  21811  mhpaddcl  21913  mdetunilem6  22339  mdetunilem9  22342  ghmcnp  23839  tgpt0  23843  qustgpopn  23844  mdegaddle  25816  ply1rem  25905  gsumsubg  32456  ogrpinv0le  32491  ogrpaddltrbid  32496  ogrpinv0lt  32498  ogrpinvlt  32499  cyc3genpmlem  32568  isarchi3  32591  archirngz  32593  archiabllem1b  32596  freshmansdream  32639  orngsqr  32680  ornglmulle  32681  orngrmulle  32682  ofldchr  32690  qusker  32722  grplsm0l  32775  quslsm  32778  mxidlprm  32848  dimkerim  32988  matunitlindflem1  36787  lfl0f  38242  lfladd0l  38247  lkrlss  38268  lkrin  38337  dvhgrp  40281  baerlem3lem1  40881  mapdh6bN  40911  hdmap1l6b  40985  hdmapinvlem3  41094  hdmapinvlem4  41095  hdmapglem7b  41102  fsuppind  41464  fsuppssind  41467