Theorem grprid 17880

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1520   ∈ wcel 2079  ‘cfv 6217  (class class class)co 7007  Basecbs 16300  +_gcplusg 16382  0_gc0g 16530  Mndcmnd 17721  Grpcgrp 17849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-iota 6181  df-fun 6219  df-fv 6225  df-riota 6968  df-ov 7010  df-0g 16532  df-mgm 17669  df-sgrp 17711  df-mnd 17722  df-grp 17852

This theorem is referenced by:  grprcan  17882  grpinvid1  17899  grpinvid2  17900  grpidinv2  17903  grpasscan2  17908  grpidrcan  17909  grpsubid1  17929  grpsubadd  17932  grppncan  17935  mulgaddcom  17993  mulgdirlem  18000  mulgmodid  18008  nmzsubg  18062  0nsg  18066  cntzsubg  18196  cayleylem2  18260  odbezout  18403  lsmdisj2  18523  pj1lid  18542  frgpuplem  18613  abladdsub4  18647  odadd2  18680  gex2abl  18682  ringlz  19015  isabvd  19269  lmod0vrid  19343  lmodfopne  19350  islmhm2  19488  mplcoe1  19921  mhpinvcl  20010  lsmcss  20506  mdetero  20891  mdetunilem6  20898  opnsubg  22387  tgpconncompeqg  22391  snclseqg  22395  clmvz  23386  deg1add  24368  ogrpaddltbi  30349  ogrpinvlt  30354  archiabllem2a  30419  archiabllem2c  30420  gsumsubg  30450  lindsunlem  30579  lflmul  35685  cdlemn4  37815  mapdh6cN  38355  hdmap1l6c  38429  hdmapinvlem3  38537  hdmapinvlem4  38538  hdmapglem7b  38545  rnglz  43587