Theorem grplid 17653

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ‘cfv 6049  (class class class)co 6813  Basecbs 16059  +_gcplusg 16143  0_gc0g 16302  Mndcmnd 17495  Grpcgrp 17623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-riota 6774  df-ov 6816  df-0g 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-grp 17626

This theorem is referenced by:  grprcan  17656  grpid  17658  isgrpid2  17659  grprinv  17670  grpinvid1  17671  grpinvid2  17672  grpidinv2  17675  grpinvid  17677  grplcan  17678  grpasscan1  17679  grpidlcan  17682  grplmulf1o  17690  grpidssd  17692  grpinvadd  17694  grpinvval2  17699  grplactcnv  17719  imasgrp  17732  mulgaddcom  17765  mulgdirlem  17773  subg0  17801  issubg2  17810  issubg4  17814  0subg  17820  isnsg3  17829  nmzsubg  17836  ssnmz  17837  eqger  17845  eqgid  17847  qusgrp  17850  qus0  17853  ghmid  17867  conjghm  17892  conjnmz  17895  subgga  17933  cntzsubg  17969  sylow1lem2  18214  sylow2blem2  18236  sylow2blem3  18237  sylow3lem1  18242  lsmmod  18288  lsmdisj2  18295  pj1rid  18315  abladdsub4  18419  ablpncan2  18421  ablpnpcan  18425  ablnncan  18426  odadd1  18451  odadd2  18452  oddvdssubg  18458  dprdfadd  18619  pgpfac1lem3a  18675  ringlz  18787  ringrz  18788  isabvd  19022  lmod0vlid  19095  lmod0vs  19098  psr0lid  19597  mplsubglem  19636  mplcoe1  19667  evpmodpmf1o  20144  ocvlss  20218  lsmcss  20238  mdetunilem6  20625  mdetunilem9  20628  ghmcnp  22119  tgpt0  22123  qustgpopn  22124  mdegaddle  24033  ply1rem  24122  ogrpinvOLD  30024  ogrpinv0le  30025  ogrpaddltrbid  30030  ogrpinv0lt  30032  ogrpinvlt  30033  isarchi3  30050  archirngz  30052  archiabllem1b  30055  orngsqr  30113  ornglmulle  30114  orngrmulle  30115  ofldchr  30123  matunitlindflem1  33718  lfl0f  34859  lfladd0l  34864  lkrlss  34885  lkrin  34954  dvhgrp  36898  baerlem3lem1  37498  mapdh6bN  37528  hdmap1l6b  37603  hdmapinvlem3  37714  hdmapinvlem4  37715  hdmapglem7b  37722  rnglz  42394