Theorem mndideu

Description: The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of Herstein p. 55. (Contributed by Mario Carneiro, 8-Dec-2014)

	Ref	Expression
Hypotheses	mndcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mndcl.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	mndideu	⊢ ( 𝐺 ∈ Mnd → ∃! 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndcl.p	⊢ + = ( +g ‘ 𝐺 )
3	1 2	mndid	⊢ ( 𝐺 ∈ Mnd → ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) )
4		mgmidmo	⊢ ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 )
5		reu5	⊢ ( ∃! 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ↔ ( ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ) )
6	3 4 5	sylanblrc	⊢ ( 𝐺 ∈ Mnd → ∃! 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) )