This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑀 = 𝑁 )