Theorem mndlid 18863

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

Hypotheses

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

Assertion

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

Proof of Theorem mndlid

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 18862	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
5	4	simpld 500	1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  0_gc0g 17530  Mndcmnd 18842

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-riota 7374  df-ov 7420  df-0g 17532  df-mgm 18736  df-sgrp 18827  df-mnd 18843

This theorem is used by:  issubmnd  18872  ress0gOLD  18874  submnd0OLD  18876  mndinvmod  18877  mndpsuppss  18878  prdsidlem  18882  imasmnd  18888  xpsmnd0  18891  mndvlid  18913  0subm  18932  0mhm  18934  mndind  18943  gsumccat  18956  dfgrp2  19092  grplid  19097  dfgrp3  19168  mhmid  19192  mhmmnd  19193  mulgnn0p1  19214  mulgnn0z  19230  mulgnn0dir  19233  cntzsubm  19471  oppgmnd  19487  odmodnn0  19673  lsmub2x  19780  mulgnn0di  19958  gsumval3  20040  gsumzaddlem  20054  gsumzsplit  20060  omndmul2  20266  omndmul3  20267  srgbinomlem4  20374  c0mgm  20606  c0mhm  20607  c0snmgmhm  20609  dsmmacl  21960  dmatmul  22725  mndifsplit  22864  tsmssplit  24384  mndlrinv  33472  mndlactf1  33474  mndlactfo  33475  mndlactf1o  33478  mndractf1o  33479  gsumwun  33524  cntzsnid  33528  slmd0vlid  33670  mndmolinv  42969  primrootsunit1  42971  primrootscoprmpow  42973  primrootscoprbij  42976  cznrng  49184  mndtccatid  50521