Theorem grprid 19208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  0_gc0g 17639  Mndcmnd 18952  Grpcgrp 19173

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566  df-riota 7400  df-ov 7446  df-0g 17641  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176

This theorem is used by:  grpridd  19210  grpinvid1  19231  grpinvid2  19232  grpidinv2  19237  grpasscan2  19242  grpidrcan  19243  grpraddf1o  19253  grpsubid1  19264  grpsubadd  19267  grppncan  19270  mulgaddcom  19337  mulgdirlem  19344  mulgmodid  19352  nmzsubg  19404  0nsg  19408  ghmquskerlem1  19527  cntzsubg  19583  cayleylem2  19657  odbezout  19802  lsmdisj2  19926  pj1lid  19945  frgpuplem  20016  abladdsub4  20055  odadd2  20093  gex2abl  20095  ogrpaddltbi  20383  ogrpinvlt  20388  rnglz  20417  isabvd  21099  lmod0vrid  21198  lmodfopne  21205  islmhm2  21343  rnglidl0  21539  lsmcss  22028  mplcoe1  22376  mdetero  22955  mdetunilem6  22962  opnsubg  24457  tgpconncompeqg  24461  snclseqg  24465  clmvz  25462  deg1add  26451  gsumsubg  33677  archiabllem2a  33825  archiabllem2c  33826  lindsunlem  34326  lflmul  40317  cdlemn4  42447  mapdh6cN  42987  hdmap1l6c  43061  hdmapinvlem3  43169  hdmapinvlem4  43170  hdmapglem7b  43177  fsuppind  43811