Theorem mndrid 18823

Description: The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.)

Hypotheses

Ref	Expression
mndlrid.b	⊢ 𝐵 = (Base‘𝐺)
mndlrid.p	⊢ + = (+g‘𝐺)
mndlrid.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
mndrid	⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)

Proof of Theorem mndrid

Step	Hyp	Ref	Expression
1		mndlrid.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2		mndlrid.p	. . 3 ⊢ + = (+g‘𝐺)
3		mndlrid.o	. . 3 ⊢ 0 = (0g‘𝐺)
4	1, 2, 3	mndlrid 18821	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
5	4	simprd 501	1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7416  Basecbs 17279  +_gcplusg 17320  0_gc0g 17502  Mndcmnd 18802

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 5260  ax-nul 5272  ax-pr 5407

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 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-br 5113  df-opab 5177  df-mpt 5196  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-iota 6496  df-fun 6542  df-fv 6548  df-riota 7373  df-ov 7419  df-0g 17504  df-mgm 18708  df-sgrp 18787  df-mnd 18803

This theorem is used by:  mndpfo  18825  issubmnd  18829  ress0g  18830  submnd0  18831  mndinvmod  18832  prdsidlem  18837  imasmnd  18843  xpsmnd0  18846  mndvrid  18868  mndind  18897  gsumccat  18910  grprid  19045  mhmid  19139  mhmmnd  19140  mulgnn0dir  19180  cntzsubm  19418  oppgmnd  19434  lsmub1x  19726  gsumval3  19987  gsumzsplit  20007  srgbinomlem3  20320  mndifsplit  22808  gsummatr01  22831  smadiadet  22842  pmatcollpw3fi1lem1  22958  chfacfscmulgsum  23032  chfacfpmmulgsum  23036  tsmssplit  24324  tsmsxp  24327  mndlrinv  33357  mndractf1  33361  mndractfo  33362  mndlactf1o  33363  mndractf1o  33364  gsummptres  33385  gsummptres2  33386  cntzsnid  33413  slmd0vrid  33556  mndmolinv  42894  primrootscoprbij  42901  aks6d1c1  42915  aks6d1c2lem3  42925  mndtccatid  50397