Theorem grprid 18998

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  0_gc0g 17485  Mndcmnd 18759  Grpcgrp 18963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-riota 7387  df-ov 7433  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966

This theorem is referenced by:  grpridd  19000  grpinvid1  19021  grpinvid2  19022  grpidinv2  19027  grpasscan2  19032  grpidrcan  19033  grpraddf1o  19044  grpsubid1  19055  grpsubadd  19058  grppncan  19061  mulgaddcom  19128  mulgdirlem  19135  mulgmodid  19143  nmzsubg  19195  0nsg  19199  ghmquskerlem1  19313  cntzsubg  19369  cayleylem2  19445  odbezout  19590  lsmdisj2  19714  pj1lid  19733  frgpuplem  19804  abladdsub4  19843  odadd2  19881  gex2abl  19883  rnglz  20182  isabvd  20829  lmod0vrid  20907  lmodfopne  20914  islmhm2  21054  rnglidl0  21256  lsmcss  21727  mplcoe1  22072  mdetero  22631  mdetunilem6  22638  opnsubg  24131  tgpconncompeqg  24135  snclseqg  24139  clmvz  25157  deg1add  26156  gsumsubg  33031  ogrpaddltbi  33077  ogrpinvlt  33082  archiabllem2a  33183  archiabllem2c  33184  lindsunlem  33651  lflmul  39049  cdlemn4  41180  mapdh6cN  41720  hdmap1l6c  41794  hdmapinvlem3  41902  hdmapinvlem4  41903  hdmapglem7b  41910  fsuppind  42576