Theorem grplid 19065

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  0_gc0g 17517  Mndcmnd 18821  Grpcgrp 19031

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-riota 7380  df-ov 7426  df-0g 17519  df-mgm 18723  df-sgrp 18806  df-mnd 18822  df-grp 19034

This theorem is used by:  grplidd  19067  grprcan  19071  grpid  19073  isgrpid2  19074  grprinv  19088  grpinvid1  19089  grpinvid2  19090  grpidinv2  19095  grpinvid  19097  grplcan  19098  grpasscan1  19099  grpidlcan  19102  grplmulf1o  19110  grpidssd  19113  grpinvadd  19115  grpinvval2  19120  grplactcnv  19140  imasgrp  19153  mulgaddcom  19195  mulgdirlem  19202  subg0  19229  issubg2  19239  issubg4  19243  isnsg3  19257  nmzsubg  19262  ssnmz  19263  eqgid  19279  qusgrp  19288  qus0  19291  ghmid  19323  conjghm  19350  subgga  19401  cntzsubg  19440  sylow1lem2  19700  sylow2blem2  19722  sylow2blem3  19723  sylow3lem1  19728  lsmmod  19776  lsmdisj2  19783  pj1rid  19803  abladdsub4  19912  ablpncan2  19916  ablpnpcan  19920  ablnncan  19921  odadd1  19949  odadd2  19950  oddvdssubg  19956  dprdfadd  20123  pgpfac1lem3a  20179  ogrpinv0le  20237  ogrpaddltrbid  20242  ogrpinv0lt  20244  ogrpinvlt  20245  rnglz  20274  rngrz  20275  isabvd  20952  orngsqr  21006  ornglmulle  21007  orngrmulle  21008  lmod0vlid  21050  lmod0vs  21053  freshmansdream  21761  evpmodpmf1o  21783  ocvlss  21859  lsmcss  21879  psr0lid  22140  mplsubglem  22185  mplcoe1  22225  mdetunilem6  22811  mdetunilem9  22814  ghmcnp  24309  tgpt0  24313  qustgpopn  24314  mdegaddle  26268  ply1rem  26360  gsumsubg  33397  cyc3genpmlem  33502  isarchi3  33538  archirngz  33540  archiabllem1b  33543  qusker  33700  grplsm0l  33743  quslsm  33745  mxidlprm  33784  matunitlindflem1  38307  lfl0f  39883  lfladd0l  39888  lkrlss  39909  lkrin  39978  dvhgrp  41921  baerlem3lem1  42521  mapdh6bN  42551  hdmap1l6b  42625  hdmapinvlem3  42734  hdmapinvlem4  42735  hdmapglem7b  42742  fsuppind  43362  fsuppssind  43365