Theorem mndlrid

Description: A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011)

	Ref	Expression
Hypotheses	mndlrid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mndlrid.p	⊢ + = ( +g ‘ 𝐺 )
	mndlrid.o	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	mndlrid	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mndlrid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndlrid.p	⊢ + = ( +g ‘ 𝐺 )
3		mndlrid.o	⊢ 0 = ( 0g ‘ 𝐺 )
4	1 2	mndid	⊢ ( 𝐺 ∈ Mnd → ∃ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) )
5	1 3 2 4	mgmlrid	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) )