Theorem grplid 19035

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  0_gc0g 17493  Mndcmnd 18793  Grpcgrp 19001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-riota 7369  df-ov 7415  df-0g 17495  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-grp 19004

This theorem is referenced by:  grplidd  19037  grprcan  19041  grpid  19043  isgrpid2  19044  grprinv  19058  grpinvid1  19059  grpinvid2  19060  grpidinv2  19065  grpinvid  19067  grplcan  19068  grpasscan1  19069  grpidlcan  19072  grplmulf1o  19080  grpidssd  19083  grpinvadd  19085  grpinvval2  19090  grplactcnv  19110  imasgrp  19123  mulgaddcom  19165  mulgdirlem  19172  subg0  19199  issubg2  19209  issubg4  19213  isnsg3  19227  nmzsubg  19232  ssnmz  19233  eqgid  19249  qusgrp  19258  qus0  19261  ghmid  19293  conjghm  19320  subgga  19371  cntzsubg  19410  sylow1lem2  19670  sylow2blem2  19692  sylow2blem3  19693  sylow3lem1  19698  lsmmod  19746  lsmdisj2  19753  pj1rid  19773  abladdsub4  19882  ablpncan2  19886  ablpnpcan  19890  ablnncan  19891  odadd1  19919  odadd2  19920  oddvdssubg  19926  dprdfadd  20093  pgpfac1lem3a  20149  ogrpinv0le  20207  ogrpaddltrbid  20212  ogrpinv0lt  20214  ogrpinvlt  20215  rnglz  20244  rngrz  20245  isabvd  20896  orngsqr  20950  ornglmulle  20951  orngrmulle  20952  lmod0vlid  20994  lmod0vs  20997  freshmansdream  21705  evpmodpmf1o  21727  ocvlss  21803  lsmcss  21823  psr0lid  22084  mplsubglem  22129  mplcoe1  22169  mdetunilem6  22755  mdetunilem9  22758  ghmcnp  24253  tgpt0  24257  qustgpopn  24258  mdegaddle  26212  ply1rem  26304  gsumsubg  33344  cyc3genpmlem  33449  isarchi3  33485  archirngz  33487  archiabllem1b  33490  qusker  33647  grplsm0l  33690  quslsm  33692  mxidlprm  33731  matunitlindflem1  38245  lfl0f  39821  lfladd0l  39826  lkrlss  39847  lkrin  39916  dvhgrp  41859  baerlem3lem1  42459  mapdh6bN  42489  hdmap1l6b  42563  hdmapinvlem3  42672  hdmapinvlem4  42673  hdmapglem7b  42680  fsuppind  43302  fsuppssind  43305