Theorem grplid 19207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  0_gc0g 17639  Mndcmnd 18952  Grpcgrp 19173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566  df-riota 7400  df-ov 7446  df-0g 17641  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176

This theorem is used by:  grplidd  19209  grprcan  19213  grpid  19215  isgrpid2  19216  grprinv  19230  grpinvid1  19231  grpinvid2  19232  grpidinv2  19237  grpinvid  19239  grplcan  19240  grpasscan1  19241  grpidlcan  19244  grplmulf1o  19252  grpidssd  19255  grpinvadd  19257  grpinvval2  19262  grplactcnv  19282  imasgrp  19295  mulgaddcom  19337  mulgdirlem  19344  subg0  19371  issubg2  19381  issubg4  19385  isnsg3  19399  nmzsubg  19404  ssnmz  19405  eqgid  19421  qusgrp  19430  qus0  19433  ghmid  19465  conjghm  19492  subgga  19544  cntzsubg  19583  sylow1lem2  19843  sylow2blem2  19865  sylow2blem3  19866  sylow3lem1  19871  lsmmod  19919  lsmdisj2  19926  pj1rid  19946  abladdsub4  20055  ablpncan2  20059  ablpnpcan  20063  ablnncan  20064  odadd1  20092  odadd2  20093  oddvdssubg  20099  dprdfadd  20266  pgpfac1lem3a  20322  ogrpinv0le  20380  ogrpaddltrbid  20385  ogrpinv0lt  20387  ogrpinvlt  20388  rnglz  20417  rngrz  20418  isabvd  21099  orngsqr  21153  ornglmulle  21154  orngrmulle  21155  lmod0vlid  21197  lmod0vs  21200  freshmansdream  21910  evpmodpmf1o  21932  ocvlss  22008  lsmcss  22028  psr0lid  22291  mplsubglem  22336  mplcoe1  22376  mdetunilem6  22962  mdetunilem9  22965  matunitlindflem1  23024  ghmcnp  24464  tgpt0  24468  qustgpopn  24469  mdegaddle  26422  ply1rem  26514  gsumsubg  33677  cyc3genpmlem  33782  isarchi3  33818  archirngz  33820  archiabllem1b  33823  qusker  33980  grplsm0l  34024  quslsm  34026  mxidlprm  34065  lfl0f  40318  lfladd0l  40323  lkrlss  40344  lkrin  40413  dvhgrp  42356  baerlem3lem1  42956  mapdh6bN  42986  hdmap1l6b  43060  hdmapinvlem3  43169  hdmapinvlem4  43170  hdmapglem7b  43177  fsuppind  43811  fsuppssind  43814