Theorem mndlid 18768

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ‘cfv 6560  (class class class)co 7432  Basecbs 17248  +_gcplusg 17298  0_gc0g 17485  Mndcmnd 18748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-iota 6513  df-fun 6562  df-fv 6568  df-riota 7389  df-ov 7435  df-0g 17487  df-mgm 18654  df-sgrp 18733  df-mnd 18749

This theorem is referenced by:  issubmnd  18775  ress0g  18776  submnd0  18777  mndinvmod  18778  mndpsuppss  18779  prdsidlem  18783  imasmnd  18789  xpsmnd0  18792  mndvlid  18813  0subm  18831  0mhm  18833  mndind  18842  gsumccat  18855  dfgrp2  18981  grplid  18986  dfgrp3  19058  mhmid  19082  mhmmnd  19083  mulgnn0p1  19104  mulgnn0z  19120  mulgnn0dir  19123  cntzsubm  19357  oppgmnd  19374  odmodnn0  19559  lsmub2x  19666  mulgnn0di  19844  gsumval3  19926  gsumzaddlem  19940  gsumzsplit  19946  srgbinomlem4  20227  c0mgm  20460  c0mhm  20461  c0snmgmhm  20463  dsmmacl  21762  dmatmul  22504  mndifsplit  22643  tsmssplit  24161  mndlrinv  33030  mndlactf1  33032  mndlactfo  33033  mndlactf1o  33036  mndractf1o  33037  gsumwun  33069  cntzsnid  33073  omndmul2  33090  omndmul3  33091  slmd0vlid  33229  mndmolinv  42097  primrootsunit1  42099  primrootscoprmpow  42101  primrootscoprbij  42104  cznrng  48182  mndtccatid  49239