Theorem grprid 19036

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  0_gc0g 17493  Mndcmnd 18793  Grpcgrp 19001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-riota 7369  df-ov 7415  df-0g 17495  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-grp 19004

This theorem is referenced by:  grpridd  19038  grpinvid1  19059  grpinvid2  19060  grpidinv2  19065  grpasscan2  19070  grpidrcan  19071  grpraddf1o  19081  grpsubid1  19092  grpsubadd  19095  grppncan  19098  mulgaddcom  19165  mulgdirlem  19172  mulgmodid  19180  nmzsubg  19232  0nsg  19236  ghmquskerlem1  19354  cntzsubg  19410  cayleylem2  19484  odbezout  19629  lsmdisj2  19753  pj1lid  19772  frgpuplem  19843  abladdsub4  19882  odadd2  19920  gex2abl  19922  ogrpaddltbi  20210  ogrpinvlt  20215  rnglz  20244  isabvd  20896  lmod0vrid  20995  lmodfopne  21002  islmhm2  21140  rnglidl0  21336  lsmcss  21823  mplcoe1  22169  mdetero  22748  mdetunilem6  22755  opnsubg  24246  tgpconncompeqg  24250  snclseqg  24254  clmvz  25251  deg1add  26241  gsumsubg  33344  archiabllem2a  33492  archiabllem2c  33493  lindsunlem  33992  lflmul  39820  cdlemn4  41950  mapdh6cN  42490  hdmap1l6c  42564  hdmapinvlem3  42672  hdmapinvlem4  42673  hdmapglem7b  42680  fsuppind  43302