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) (Proof shortened by AV, 18-Aug-2026)

	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	3	mgmideud	⊢ ( 𝐺 ∈ Mnd → ∃! 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) )