Theorem mndid

Description: A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndcl.p	⊢ + = ( +g ‘ 𝐺 )
3	1 2	ismnd	⊢ ( 𝐺 ∈ Mnd ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ) )
4	3	simprbi	⊢ ( 𝐺 ∈ Mnd → ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) )