Theorem mndlid 18681

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  0_gc0g 17402  Mndcmnd 18661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-riota 7344  df-ov 7390  df-0g 17404  df-mgm 18567  df-sgrp 18646  df-mnd 18662

This theorem is referenced by:  issubmnd  18688  ress0g  18689  submnd0  18690  mndinvmod  18691  mndpsuppss  18692  prdsidlem  18696  imasmnd  18702  xpsmnd0  18705  mndvlid  18726  0subm  18744  0mhm  18746  mndind  18755  gsumccat  18768  dfgrp2  18894  grplid  18899  dfgrp3  18971  mhmid  18995  mhmmnd  18996  mulgnn0p1  19017  mulgnn0z  19033  mulgnn0dir  19036  cntzsubm  19270  oppgmnd  19286  odmodnn0  19470  lsmub2x  19577  mulgnn0di  19755  gsumval3  19837  gsumzaddlem  19851  gsumzsplit  19857  srgbinomlem4  20138  c0mgm  20368  c0mhm  20369  c0snmgmhm  20371  dsmmacl  21650  dmatmul  22384  mndifsplit  22523  tsmssplit  24039  mndlrinv  32965  mndlactf1  32967  mndlactfo  32968  mndlactf1o  32971  mndractf1o  32972  gsumwun  33005  cntzsnid  33009  omndmul2  33026  omndmul3  33027  slmd0vlid  33175  mndmolinv  42083  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  cznrng  48246  mndtccatid  49573