Theorem grplid 17659

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ‘cfv 6030  (class class class)co 6795  Basecbs 16063  +_gcplusg 16148  0_gc0g 16307  Mndcmnd 17501  Grpcgrp 17629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-iota 5993  df-fun 6032  df-fv 6038  df-riota 6756  df-ov 6798  df-0g 16309  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-grp 17632

This theorem is referenced by:  grprcan  17662  grpid  17664  isgrpid2  17665  grprinv  17676  grpinvid1  17677  grpinvid2  17678  grpidinv2  17681  grpinvid  17683  grplcan  17684  grpasscan1  17685  grpidlcan  17688  grplmulf1o  17696  grpidssd  17698  grpinvadd  17700  grpinvval2  17705  grplactcnv  17725  imasgrp  17738  mulgaddcom  17771  mulgdirlem  17779  subg0  17807  issubg2  17816  issubg4  17820  0subg  17826  isnsg3  17835  nmzsubg  17842  ssnmz  17843  eqger  17851  eqgid  17853  qusgrp  17856  qus0  17859  ghmid  17873  conjghm  17898  conjnmz  17901  subgga  17939  cntzsubg  17975  sylow1lem2  18220  sylow2blem2  18242  sylow2blem3  18243  sylow3lem1  18248  lsmmod  18294  lsmdisj2  18301  pj1rid  18321  abladdsub4  18425  ablpncan2  18427  ablpnpcan  18431  ablnncan  18432  odadd1  18457  odadd2  18458  oddvdssubg  18464  dprdfadd  18626  pgpfac1lem3a  18682  ringlz  18794  ringrz  18795  isabvd  19029  lmod0vlid  19102  lmod0vs  19105  psr0lid  19609  mplsubglem  19648  mplcoe1  19679  evpmodpmf1o  20157  ocvlss  20232  lsmcss  20252  mdetunilem6  20640  mdetunilem9  20643  ghmcnp  22137  tgpt0  22141  qustgpopn  22142  mdegaddle  24053  ply1rem  24142  ogrpinvOLD  30054  ogrpinv0le  30055  ogrpaddltrbid  30060  ogrpinv0lt  30062  ogrpinvlt  30063  isarchi3  30080  archirngz  30082  archiabllem1b  30085  orngsqr  30143  ornglmulle  30144  orngrmulle  30145  ofldchr  30153  matunitlindflem1  33737  lfl0f  34877  lfladd0l  34882  lkrlss  34903  lkrin  34972  dvhgrp  36917  baerlem3lem1  37517  mapdh6bN  37547  hdmap1l6b  37621  hdmapinvlem3  37730  hdmapinvlem4  37731  hdmapglem7b  37738  rnglz  42409