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 
|- B = ( Base ` E )
mndlrinv.z 
|- .0. = ( 0g ` E )
mndlrinv.p 
|- .+ = ( +g ` E )
mndlrinv.e 
|- ( ph -> E e. Mnd )
mndlrinv.x 
|- ( ph -> X e. B )
mndlrinv.m 
|- ( ph -> M e. B )
mndlrinv.n 
|- ( ph -> N e. B )
mndlrinv.1 
|- ( ph -> ( M .+ X ) = .0. )
mndlrinv.2 
|- ( ph -> ( X .+ N ) = .0. )
Assertion mndlrinv 
|- ( ph -> M = N )

Proof

Step Hyp Ref Expression
1 mndlrinv.b 
 |-  B = ( Base ` E )
2 mndlrinv.z 
 |-  .0. = ( 0g ` E )
3 mndlrinv.p 
 |-  .+ = ( +g ` E )
4 mndlrinv.e 
 |-  ( ph -> E e. Mnd )
5 mndlrinv.x 
 |-  ( ph -> X e. B )
6 mndlrinv.m 
 |-  ( ph -> M e. B )
7 mndlrinv.n 
 |-  ( ph -> N e. B )
8 mndlrinv.1 
 |-  ( ph -> ( M .+ X ) = .0. )
9 mndlrinv.2 
 |-  ( ph -> ( X .+ N ) = .0. )
10 1 3 4 6 5 7 mndassd 
 |-  ( ph -> ( ( M .+ X ) .+ N ) = ( M .+ ( X .+ N ) ) )
11 8 oveq1d 
 |-  ( ph -> ( ( M .+ X ) .+ N ) = ( .0. .+ N ) )
12 9 oveq2d 
 |-  ( ph -> ( M .+ ( X .+ N ) ) = ( M .+ .0. ) )
13 10 11 12 3eqtr3rd 
 |-  ( ph -> ( M .+ .0. ) = ( .0. .+ N ) )
14 1 3 2 mndrid 
 |-  ( ( E e. Mnd /\ M e. B ) -> ( M .+ .0. ) = M )
15 4 6 14 syl2anc 
 |-  ( ph -> ( M .+ .0. ) = M )
16 1 3 2 mndlid 
 |-  ( ( E e. Mnd /\ N e. B ) -> ( .0. .+ N ) = N )
17 4 7 16 syl2anc 
 |-  ( ph -> ( .0. .+ N ) = N )
18 13 15 17 3eqtr3d 
 |-  ( ph -> M = N )