Theorem grplid 19178

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  +_gcplusg 17428  0_gc0g 17610  Mndcmnd 18923  Grpcgrp 19144

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-riota 7377  df-ov 7423  df-0g 17612  df-mgm 18816  df-sgrp 18908  df-mnd 18924  df-grp 19147

This theorem is used by:  grplidd  19180  grprcan  19184  grpid  19186  isgrpid2  19187  grprinv  19201  grpinvid1  19202  grpinvid2  19203  grpidinv2  19208  grpinvid  19210  grplcan  19211  grpasscan1  19212  grpidlcan  19215  grplmulf1o  19223  grpidssd  19226  grpinvadd  19228  grpinvval2  19233  grplactcnv  19253  imasgrp  19266  mulgaddcom  19308  mulgdirlem  19315  subg0  19342  issubg2  19352  issubg4  19356  isnsg3  19370  nmzsubg  19375  ssnmz  19376  eqgid  19392  qusgrp  19401  qus0  19404  ghmid  19436  conjghm  19463  subgga  19514  cntzsubg  19553  sylow1lem2  19813  sylow2blem2  19835  sylow2blem3  19836  sylow3lem1  19841  lsmmod  19889  lsmdisj2  19896  pj1rid  19916  abladdsub4  20025  ablpncan2  20029  ablpnpcan  20033  ablnncan  20034  odadd1  20062  odadd2  20063  oddvdssubg  20069  dprdfadd  20236  pgpfac1lem3a  20292  ogrpinv0le  20350  ogrpaddltrbid  20355  ogrpinv0lt  20357  ogrpinvlt  20358  rnglz  20387  rngrz  20388  isabvd  21069  orngsqr  21123  ornglmulle  21124  orngrmulle  21125  lmod0vlid  21167  lmod0vs  21170  freshmansdream  21880  evpmodpmf1o  21902  ocvlss  21978  lsmcss  21998  psr0lid  22261  mplsubglem  22306  mplcoe1  22346  mdetunilem6  22932  mdetunilem9  22935  matunitlindflem1  22994  ghmcnp  24434  tgpt0  24438  qustgpopn  24439  mdegaddle  26392  ply1rem  26484  gsumsubg  33607  cyc3genpmlem  33712  isarchi3  33748  archirngz  33750  archiabllem1b  33753  qusker  33910  grplsm0l  33954  quslsm  33956  mxidlprm  33995  lfl0f  40127  lfladd0l  40132  lkrlss  40153  lkrin  40222  dvhgrp  42165  baerlem3lem1  42765  mapdh6bN  42795  hdmap1l6b  42869  hdmapinvlem3  42978  hdmapinvlem4  42979  hdmapglem7b  42986  fsuppind  43619  fsuppssind  43622