Theorem mndlid 18924

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 18923	. 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 6531  (class class class)co 7412  Basecbs 17367  +_gcplusg 17408  0_gc0g 17590  Mndcmnd 18903

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 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-riota 7369  df-ov 7415  df-0g 17592  df-mgm 18796  df-sgrp 18888  df-mnd 18904

This theorem is used by:  issubmnd  18933  ress0gOLD  18935  submnd0OLD  18937  mndinvmod  18938  mndpsuppss  18939  prdsidlem  18943  imasmnd  18949  xpsmnd0  18952  mndvlid  18974  0subm  18993  0mhm  18995  mndind  19004  gsumccat  19017  dfgrp2  19153  grplid  19158  dfgrp3  19229  mhmid  19253  mhmmnd  19254  mulgnn0p1  19275  mulgnn0z  19291  mulgnn0dir  19294  cntzsubm  19532  oppgmnd  19548  odmodnn0  19734  lsmub2x  19841  mulgnn0di  20019  gsumval3  20101  gsumzaddlem  20115  gsumzsplit  20121  omndmul2  20327  omndmul3  20328  srgbinomlem4  20435  c0mgm  20669  c0mhm  20670  c0snmgmhm  20672  dsmmacl  22027  dmatmul  22792  mndifsplit  22931  tsmssplit  24451  mndlrinv  33567  mndlactf1  33569  mndlactfo  33570  mndlactf1o  33573  mndractf1o  33574  gsumwun  33619  cntzsnid  33623  slmd0vlid  33765  mndmolinv  43113  primrootsunit1  43115  primrootscoprmpow  43117  primrootscoprbij  43120  cznrng  49302  mndtccatid  50639