Theorem mndlid 18822

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 18821	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
5	4	simpld 500	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:  issubmnd  18829  ress0g  18830  submnd0  18831  mndinvmod  18832  mndpsuppss  18833  prdsidlem  18837  imasmnd  18843  xpsmnd0  18846  mndvlid  18867  0subm  18886  0mhm  18888  mndind  18897  gsumccat  18910  dfgrp2  19039  grplid  19044  dfgrp3  19115  mhmid  19139  mhmmnd  19140  mulgnn0p1  19161  mulgnn0z  19177  mulgnn0dir  19180  cntzsubm  19418  oppgmnd  19434  odmodnn0  19620  lsmub2x  19727  mulgnn0di  19905  gsumval3  19987  gsumzaddlem  20001  gsumzsplit  20007  omndmul2  20213  omndmul3  20214  srgbinomlem4  20321  c0mgm  20552  c0mhm  20553  c0snmgmhm  20555  dsmmacl  21906  dmatmul  22669  mndifsplit  22808  tsmssplit  24324  mndlrinv  33357  mndlactf1  33359  mndlactfo  33360  mndlactf1o  33363  mndractf1o  33364  gsumwun  33409  cntzsnid  33413  slmd0vlid  33555  mndmolinv  42894  primrootsunit1  42896  primrootscoprmpow  42898  primrootscoprbij  42901  cznrng  49058  mndtccatid  50397