Theorem grplid 17915

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2048  ‘cfv 6186  (class class class)co 6974  Basecbs 16333  +_gcplusg 16415  0_gc0g 16563  Mndcmnd 17756  Grpcgrp 17885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-iota 6150  df-fun 6188  df-fv 6194  df-riota 6935  df-ov 6977  df-0g 16565  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-grp 17888

This theorem is referenced by:  grprcan  17918  grpid  17920  isgrpid2  17921  grprinv  17934  grpinvid1  17935  grpinvid2  17936  grpidinv2  17939  grpinvid  17941  grplcan  17942  grpasscan1  17943  grpidlcan  17946  grplmulf1o  17954  grpidssd  17956  grpinvadd  17958  grpinvval2  17963  grplactcnv  17983  imasgrp  17996  mulgaddcom  18029  mulgdirlem  18036  subg0  18063  issubg2  18072  issubg4  18076  0subg  18082  isnsg3  18091  nmzsubg  18098  ssnmz  18099  eqger  18107  eqgid  18109  qusgrp  18112  qus0  18115  ghmid  18129  conjghm  18154  conjnmz  18157  subgga  18195  cntzsubg  18232  sylow1lem2  18479  sylow2blem2  18501  sylow2blem3  18502  sylow3lem1  18507  lsmmod  18553  lsmdisj2  18560  pj1rid  18580  abladdsub4  18686  ablpncan2  18688  ablpnpcan  18692  ablnncan  18693  odadd1  18718  odadd2  18719  oddvdssubg  18725  dprdfadd  18886  pgpfac1lem3a  18942  ringlz  19054  ringrz  19055  isabvd  19307  lmod0vlid  19380  lmod0vs  19383  psr0lid  19883  mplsubglem  19922  mplcoe1  19953  mhpaddcl  20038  evpmodpmf1o  20436  ocvlss  20512  lsmcss  20532  mdetunilem6  20924  mdetunilem9  20927  ghmcnp  22420  tgpt0  22424  qustgpopn  22425  mdegaddle  24365  ply1rem  24454  ogrpinvOLD  30425  ogrpinv0le  30426  ogrpaddltrbid  30431  ogrpinv0lt  30433  ogrpinvlt  30434  isarchi3  30473  archirngz  30475  archiabllem1b  30478  gsumsubg  30511  freshmansdream  30529  orngsqr  30547  ornglmulle  30548  orngrmulle  30549  ofldchr  30557  qusker  30588  dimkerim  30643  matunitlindflem1  34307  lfl0f  35628  lfladd0l  35633  lkrlss  35654  lkrin  35723  dvhgrp  37666  baerlem3lem1  38266  mapdh6bN  38296  hdmap1l6b  38370  hdmapinvlem3  38479  hdmapinvlem4  38480  hdmapglem7b  38487  rnglz  43493