Theorem grprid 18830

Description: The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)

Hypotheses

Ref	Expression
grpbn0.b	⊢ 𝐵 = (Base‘𝐺)
grplid.p	⊢ + = (+g‘𝐺)
grplid.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
grprid	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)

Proof of Theorem grprid

Step	Hyp	Ref	Expression
1		grpmnd 18803	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpbn0.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grplid.p	. . 3 ⊢ + = (+g‘𝐺)
4		grplid.o	. . 3 ⊢ 0 = (0g‘𝐺)
5	2, 3, 4	mndrid 18625	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
6	1, 5	sylan 580	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ‘cfv 6533  (class class class)co 7394  Basecbs 17128  +_gcplusg 17181  0_gc0g 17369  Mndcmnd 18604  Grpcgrp 18796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pr 5421

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-iota 6485  df-fun 6535  df-fv 6541  df-riota 7350  df-ov 7397  df-0g 17371  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-grp 18799

This theorem is referenced by:  grpridd  18832  grprcan  18835  grpinvid1  18853  grpinvid2  18854  grpidinv2  18858  grpasscan2  18863  grpidrcan  18864  grpsubid1  18884  grpsubadd  18887  grppncan  18890  mulgaddcom  18952  mulgdirlem  18959  mulgmodid  18967  nmzsubg  19019  0nsg  19023  cntzsubg  19169  cayleylem2  19247  odbezout  19392  lsmdisj2  19516  pj1lid  19535  frgpuplem  19606  abladdsub4  19644  odadd2  19679  gex2abl  19681  ringlz  20066  isabvd  20379  lmod0vrid  20454  lmodfopne  20461  islmhm2  20600  lsmcss  21180  mplcoe1  21522  mdetero  22043  mdetunilem6  22050  opnsubg  23543  tgpconncompeqg  23547  snclseqg  23551  clmvz  24558  deg1add  25552  gsumsubg  32133  ogrpaddltbi  32171  ogrpinvlt  32176  archiabllem2a  32275  archiabllem2c  32276  ghmquskerlem1  32448  lindsunlem  32611  lflmul  37807  cdlemn4  39938  mapdh6cN  40478  hdmap1l6c  40552  hdmapinvlem3  40660  hdmapinvlem4  40661  hdmapglem7b  40668  fsuppind  41015  rnglz  46494