Theorem mndlid 18713

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  0_gc0g 17393  Mndcmnd 18693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7317  df-ov 7363  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694

This theorem is referenced by:  issubmnd  18720  ress0g  18721  submnd0  18722  mndinvmod  18723  mndpsuppss  18724  prdsidlem  18728  imasmnd  18734  xpsmnd0  18737  mndvlid  18758  0subm  18776  0mhm  18778  mndind  18787  gsumccat  18800  dfgrp2  18929  grplid  18934  dfgrp3  19006  mhmid  19030  mhmmnd  19031  mulgnn0p1  19052  mulgnn0z  19068  mulgnn0dir  19071  cntzsubm  19304  oppgmnd  19320  odmodnn0  19506  lsmub2x  19613  mulgnn0di  19791  gsumval3  19873  gsumzaddlem  19887  gsumzsplit  19893  omndmul2  20099  omndmul3  20100  srgbinomlem4  20201  c0mgm  20430  c0mhm  20431  c0snmgmhm  20433  dsmmacl  21731  dmatmul  22472  mndifsplit  22611  tsmssplit  24127  mndlrinv  33099  mndlactf1  33101  mndlactfo  33102  mndlactf1o  33105  mndractf1o  33106  gsumwun  33152  cntzsnid  33156  slmd0vlid  33298  mndmolinv  42548  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  cznrng  48749  mndtccatid  50074