Theorem grprid 19066

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  0_gc0g 17517  Mndcmnd 18821  Grpcgrp 19031

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-riota 7380  df-ov 7426  df-0g 17519  df-mgm 18723  df-sgrp 18806  df-mnd 18822  df-grp 19034

This theorem is used by:  grpridd  19068  grpinvid1  19089  grpinvid2  19090  grpidinv2  19095  grpasscan2  19100  grpidrcan  19101  grpraddf1o  19111  grpsubid1  19122  grpsubadd  19125  grppncan  19128  mulgaddcom  19195  mulgdirlem  19202  mulgmodid  19210  nmzsubg  19262  0nsg  19266  ghmquskerlem1  19384  cntzsubg  19440  cayleylem2  19514  odbezout  19659  lsmdisj2  19783  pj1lid  19802  frgpuplem  19873  abladdsub4  19912  odadd2  19950  gex2abl  19952  ogrpaddltbi  20240  ogrpinvlt  20245  rnglz  20274  isabvd  20952  lmod0vrid  21051  lmodfopne  21058  islmhm2  21196  rnglidl0  21392  lsmcss  21879  mplcoe1  22225  mdetero  22804  mdetunilem6  22811  opnsubg  24302  tgpconncompeqg  24306  snclseqg  24310  clmvz  25307  deg1add  26297  gsumsubg  33397  archiabllem2a  33545  archiabllem2c  33546  lindsunlem  34045  lflmul  39882  cdlemn4  42012  mapdh6cN  42552  hdmap1l6c  42626  hdmapinvlem3  42734  hdmapinvlem4  42735  hdmapglem7b  42742  fsuppind  43362