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 )