Theorem mndlrinv

Description: In a monoid, if an element X has both a left inverse M and a right inverse N , they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	mndlrinv.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	mndlrinv.z	⊢ 0 = ( 0g ‘ 𝐸 )
	mndlrinv.p	⊢ + = ( +g ‘ 𝐸 )
	mndlrinv.e	⊢ ( 𝜑 → 𝐸 ∈ Mnd )
	mndlrinv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mndlrinv.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
	mndlrinv.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
	mndlrinv.1	⊢ ( 𝜑 → ( 𝑀 + 𝑋 ) = 0 )
	mndlrinv.2	⊢ ( 𝜑 → ( 𝑋 + 𝑁 ) = 0 )
Assertion	mndlrinv	⊢ ( 𝜑 → 𝑀 = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		mndlrinv.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
2		mndlrinv.z	⊢ 0 = ( 0g ‘ 𝐸 )
3		mndlrinv.p	⊢ + = ( +g ‘ 𝐸 )
4		mndlrinv.e	⊢ ( 𝜑 → 𝐸 ∈ Mnd )
5		mndlrinv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		mndlrinv.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
7		mndlrinv.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
8		mndlrinv.1	⊢ ( 𝜑 → ( 𝑀 + 𝑋 ) = 0 )
9		mndlrinv.2	⊢ ( 𝜑 → ( 𝑋 + 𝑁 ) = 0 )
10	1 3 4 6 5 7	mndassd	⊢ ( 𝜑 → ( ( 𝑀 + 𝑋 ) + 𝑁 ) = ( 𝑀 + ( 𝑋 + 𝑁 ) ) )
11	8	oveq1d	⊢ ( 𝜑 → ( ( 𝑀 + 𝑋 ) + 𝑁 ) = ( 0 + 𝑁 ) )
12	9	oveq2d	⊢ ( 𝜑 → ( 𝑀 + ( 𝑋 + 𝑁 ) ) = ( 𝑀 + 0 ) )
13	10 11 12	3eqtr3rd	⊢ ( 𝜑 → ( 𝑀 + 0 ) = ( 0 + 𝑁 ) )
14	1 3 2	mndrid	⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 + 0 ) = 𝑀 )
15	4 6 14	syl2anc	⊢ ( 𝜑 → ( 𝑀 + 0 ) = 𝑀 )
16	1 3 2	mndlid	⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑁 ∈ 𝐵 ) → ( 0 + 𝑁 ) = 𝑁 )
17	4 7 16	syl2anc	⊢ ( 𝜑 → ( 0 + 𝑁 ) = 𝑁 )
18	13 15 17	3eqtr3d	⊢ ( 𝜑 → 𝑀 = 𝑁 )