Theorem grplid 18590

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ‘cfv 6430  (class class class)co 7268  Basecbs 16893  +_gcplusg 16943  0_gc0g 17131  Mndcmnd 18366  Grpcgrp 18558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-iota 6388  df-fun 6432  df-fv 6438  df-riota 7225  df-ov 7271  df-0g 17133  df-mgm 18307  df-sgrp 18356  df-mnd 18367  df-grp 18561

This theorem is referenced by:  grprcan  18594  grpid  18596  isgrpid2  18597  grprinv  18610  grpinvid1  18611  grpinvid2  18612  grpidinv2  18615  grpinvid  18617  grplcan  18618  grpasscan1  18619  grpidlcan  18622  grplmulf1o  18630  grpidssd  18632  grpinvadd  18634  grpinvval2  18639  grplactcnv  18659  imasgrp  18672  mulgaddcom  18708  mulgdirlem  18715  subg0  18742  issubg2  18751  issubg4  18755  0subg  18761  isnsg3  18769  nmzsubg  18774  ssnmz  18775  eqger  18787  eqgid  18789  qusgrp  18792  qus0  18795  ghmid  18821  conjghm  18846  conjnmz  18849  subgga  18887  cntzsubg  18924  sylow1lem2  19185  sylow2blem2  19207  sylow2blem3  19208  sylow3lem1  19213  lsmmod  19262  lsmdisj2  19269  pj1rid  19289  abladdsub4  19396  ablpncan2  19398  ablpnpcan  19402  ablnncan  19403  odadd1  19430  odadd2  19431  oddvdssubg  19437  dprdfadd  19604  pgpfac1lem3a  19660  ringlz  19807  ringrz  19808  isabvd  20061  lmod0vlid  20134  lmod0vs  20137  evpmodpmf1o  20782  ocvlss  20858  lsmcss  20878  psr0lid  21145  mplsubglem  21186  mplcoe1  21219  mhpaddcl  21322  mdetunilem6  21747  mdetunilem9  21750  ghmcnp  23247  tgpt0  23251  qustgpopn  23252  mdegaddle  25220  ply1rem  25309  gsumsubg  31285  ogrpinv0le  31320  ogrpaddltrbid  31325  ogrpinv0lt  31327  ogrpinvlt  31328  cyc3genpmlem  31397  isarchi3  31420  archirngz  31422  archiabllem1b  31425  freshmansdream  31463  orngsqr  31482  ornglmulle  31483  orngrmulle  31484  ofldchr  31492  qusker  31528  grplsm0l  31570  quslsm  31572  mxidlprm  31619  dimkerim  31687  matunitlindflem1  35752  lfl0f  37062  lfladd0l  37067  lkrlss  37088  lkrin  37157  dvhgrp  39100  baerlem3lem1  39700  mapdh6bN  39730  hdmap1l6b  39804  hdmapinvlem3  39913  hdmapinvlem4  39914  hdmapglem7b  39921  fsuppind  40259  fsuppssind  40262  rnglz  45394