Theorem grplid 18941

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  0_gc0g 17400  Mndcmnd 18700  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7320  df-ov 7366  df-0g 17402  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910

This theorem is referenced by:  grplidd  18943  grprcan  18947  grpid  18949  isgrpid2  18950  grprinv  18964  grpinvid1  18965  grpinvid2  18966  grpidinv2  18971  grpinvid  18973  grplcan  18974  grpasscan1  18975  grpidlcan  18978  grplmulf1o  18987  grpidssd  18990  grpinvadd  18992  grpinvval2  18997  grplactcnv  19017  imasgrp  19030  mulgaddcom  19072  mulgdirlem  19079  subg0  19106  issubg2  19115  issubg4  19119  isnsg3  19133  nmzsubg  19138  ssnmz  19139  eqgid  19153  qusgrp  19159  qus0  19162  ghmid  19195  conjghm  19222  subgga  19273  cntzsubg  19312  sylow1lem2  19572  sylow2blem2  19594  sylow2blem3  19595  sylow3lem1  19600  lsmmod  19648  lsmdisj2  19655  pj1rid  19675  abladdsub4  19784  ablpncan2  19788  ablpnpcan  19792  ablnncan  19793  odadd1  19821  odadd2  19822  oddvdssubg  19828  dprdfadd  19995  pgpfac1lem3a  20051  ogrpinv0le  20109  ogrpaddltrbid  20114  ogrpinv0lt  20116  ogrpinvlt  20117  rnglz  20144  rngrz  20145  isabvd  20791  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  lmod0vlid  20889  lmod0vs  20892  freshmansdream  21556  evpmodpmf1o  21578  ocvlss  21654  lsmcss  21674  psr0lid  21935  mplsubglem  21980  mplcoe1  22020  mdetunilem6  22607  mdetunilem9  22610  ghmcnp  24105  tgpt0  24109  qustgpopn  24110  mdegaddle  26064  ply1rem  26156  gsumsubg  33134  cyc3genpmlem  33239  isarchi3  33275  archirngz  33277  archiabllem1b  33280  qusker  33439  grplsm0l  33493  quslsm  33495  mxidlprm  33560  matunitlindflem1  37990  lfl0f  39568  lfladd0l  39573  lkrlss  39594  lkrin  39663  dvhgrp  41606  baerlem3lem1  42206  mapdh6bN  42236  hdmap1l6b  42310  hdmapinvlem3  42419  hdmapinvlem4  42420  hdmapglem7b  42427  fsuppind  43047  fsuppssind  43050