Theorem grplid 18654

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  ‘cfv 6458  (class class class)co 7307  Basecbs 16957  +_gcplusg 17007  0_gc0g 17195  Mndcmnd 18430  Grpcgrp 18622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-iota 6410  df-fun 6460  df-fv 6466  df-riota 7264  df-ov 7310  df-0g 17197  df-mgm 18371  df-sgrp 18420  df-mnd 18431  df-grp 18625

This theorem is referenced by:  grprcan  18658  grpid  18660  isgrpid2  18661  grprinv  18674  grpinvid1  18675  grpinvid2  18676  grpidinv2  18679  grpinvid  18681  grplcan  18682  grpasscan1  18683  grpidlcan  18686  grplmulf1o  18694  grpidssd  18696  grpinvadd  18698  grpinvval2  18703  grplactcnv  18723  imasgrp  18736  mulgaddcom  18772  mulgdirlem  18779  subg0  18806  issubg2  18815  issubg4  18819  0subg  18825  isnsg3  18833  nmzsubg  18838  ssnmz  18839  eqger  18851  eqgid  18853  qusgrp  18856  qus0  18859  ghmid  18885  conjghm  18910  conjnmz  18913  subgga  18951  cntzsubg  18988  sylow1lem2  19249  sylow2blem2  19271  sylow2blem3  19272  sylow3lem1  19277  lsmmod  19326  lsmdisj2  19333  pj1rid  19353  abladdsub4  19460  ablpncan2  19462  ablpnpcan  19466  ablnncan  19467  odadd1  19494  odadd2  19495  oddvdssubg  19501  dprdfadd  19668  pgpfac1lem3a  19724  ringlz  19871  ringrz  19872  isabvd  20125  lmod0vlid  20198  lmod0vs  20201  evpmodpmf1o  20846  ocvlss  20922  lsmcss  20942  psr0lid  21209  mplsubglem  21250  mplcoe1  21283  mhpaddcl  21386  mdetunilem6  21811  mdetunilem9  21814  ghmcnp  23311  tgpt0  23315  qustgpopn  23316  mdegaddle  25284  ply1rem  25373  gsumsubg  31351  ogrpinv0le  31386  ogrpaddltrbid  31391  ogrpinv0lt  31393  ogrpinvlt  31394  cyc3genpmlem  31463  isarchi3  31486  archirngz  31488  archiabllem1b  31491  freshmansdream  31529  orngsqr  31548  ornglmulle  31549  orngrmulle  31550  ofldchr  31558  qusker  31594  grplsm0l  31636  quslsm  31638  mxidlprm  31685  dimkerim  31753  matunitlindflem1  35817  lfl0f  37125  lfladd0l  37130  lkrlss  37151  lkrin  37220  dvhgrp  39163  baerlem3lem1  39763  mapdh6bN  39793  hdmap1l6b  39867  hdmapinvlem3  39976  hdmapinvlem4  39977  hdmapglem7b  39984  fsuppind  40316  fsuppssind  40319  rnglz  45500