Theorem grprid 18910

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  0_gc0g 17371  Mndcmnd 18671  Grpcgrp 18875

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-riota 7325  df-ov 7371  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878

This theorem is referenced by:  grpridd  18912  grpinvid1  18933  grpinvid2  18934  grpidinv2  18939  grpasscan2  18944  grpidrcan  18945  grpraddf1o  18956  grpsubid1  18967  grpsubadd  18970  grppncan  18973  mulgaddcom  19040  mulgdirlem  19047  mulgmodid  19055  nmzsubg  19106  0nsg  19110  ghmquskerlem1  19224  cntzsubg  19280  cayleylem2  19354  odbezout  19499  lsmdisj2  19623  pj1lid  19642  frgpuplem  19713  abladdsub4  19752  odadd2  19790  gex2abl  19792  ogrpaddltbi  20080  ogrpinvlt  20085  rnglz  20112  isabvd  20757  lmod0vrid  20856  lmodfopne  20863  islmhm2  21002  rnglidl0  21196  lsmcss  21659  mplcoe1  22004  mdetero  22566  mdetunilem6  22573  opnsubg  24064  tgpconncompeqg  24068  snclseqg  24072  clmvz  25079  deg1add  26076  gsumsubg  33139  archiabllem2a  33287  archiabllem2c  33288  lindsunlem  33801  lflmul  39438  cdlemn4  41568  mapdh6cN  42108  hdmap1l6c  42182  hdmapinvlem3  42290  hdmapinvlem4  42291  hdmapglem7b  42298  fsuppind  42942