Theorem mndlid 18737

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  0_gc0g 17458  Mndcmnd 18717

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fv 6544  df-riota 7367  df-ov 7413  df-0g 17460  df-mgm 18623  df-sgrp 18702  df-mnd 18718

This theorem is referenced by:  issubmnd  18744  ress0g  18745  submnd0  18746  mndinvmod  18747  mndpsuppss  18748  prdsidlem  18752  imasmnd  18758  xpsmnd0  18761  mndvlid  18782  0subm  18800  0mhm  18802  mndind  18811  gsumccat  18824  dfgrp2  18950  grplid  18955  dfgrp3  19027  mhmid  19051  mhmmnd  19052  mulgnn0p1  19073  mulgnn0z  19089  mulgnn0dir  19092  cntzsubm  19326  oppgmnd  19342  odmodnn0  19526  lsmub2x  19633  mulgnn0di  19811  gsumval3  19893  gsumzaddlem  19907  gsumzsplit  19913  srgbinomlem4  20194  c0mgm  20424  c0mhm  20425  c0snmgmhm  20427  dsmmacl  21706  dmatmul  22440  mndifsplit  22579  tsmssplit  24095  mndlrinv  33024  mndlactf1  33026  mndlactfo  33027  mndlactf1o  33030  mndractf1o  33031  gsumwun  33064  cntzsnid  33068  omndmul2  33085  omndmul3  33086  slmd0vlid  33224  mndmolinv  42113  primrootsunit1  42115  primrootscoprmpow  42117  primrootscoprbij  42120  cznrng  48203  mndtccatid  49431