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={\mathrm{Base}}_E$$
	mndlrinv.z	$$⊢\underset{\dot{}}{0}=0_E$$
	mndlrinv.p	$$⊢\underset{\dot{}}{+}={+}_E$$
	mndlrinv.e	$$⊢\phi \to E\in \mathrm{Mnd}$$
	mndlrinv.x	$$⊢\phi \to X\in B$$
	mndlrinv.m	$$⊢\phi \to M\in B$$
	mndlrinv.n	$$⊢\phi \to N\in B$$
	mndlrinv.1	$$⊢\phi \to M\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
	mndlrinv.2	$$⊢\phi \to X\underset{\dot{}}{+}N=\underset{\dot{}}{0}$$
Assertion	mndlrinv	$$⊢\phi \to M=N$$

Proof

Step	Hyp	Ref	Expression
1		mndlrinv.b	$$⊢B={\mathrm{Base}}_E$$
2		mndlrinv.z	$$⊢\underset{\dot{}}{0}=0_E$$
3		mndlrinv.p	$$⊢\underset{\dot{}}{+}={+}_E$$
4		mndlrinv.e	$$⊢\phi \to E\in \mathrm{Mnd}$$
5		mndlrinv.x	$$⊢\phi \to X\in B$$
6		mndlrinv.m	$$⊢\phi \to M\in B$$
7		mndlrinv.n	$$⊢\phi \to N\in B$$
8		mndlrinv.1	$$⊢\phi \to M\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
9		mndlrinv.2	$$⊢\phi \to X\underset{\dot{}}{+}N=\underset{\dot{}}{0}$$
10	1 3 4 6 5 7	mndassd	$$⊢\phi \to \left(M\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}N=M\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)$$
11	8	oveq1d	$$⊢\phi \to \left(M\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}N=\underset{\dot{}}{0}\underset{\dot{}}{+}N$$
12	9	oveq2d	$$⊢\phi \to M\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)=M\underset{\dot{}}{+}\underset{\dot{}}{0}$$
13	10 11 12	3eqtr3rd	$$⊢\phi \to M\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{+}N$$
14	1 3 2	mndrid	$$⊢\left(E\in \mathrm{Mnd}\wedge M\in B\right)\to M\underset{\dot{}}{+}\underset{\dot{}}{0}=M$$
15	4 6 14	syl2anc	$$⊢\phi \to M\underset{\dot{}}{+}\underset{\dot{}}{0}=M$$
16	1 3 2	mndlid	$$⊢\left(E\in \mathrm{Mnd}\wedge N\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}N=N$$
17	4 7 16	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}N=N$$
18	13 15 17	3eqtr3d	$$⊢\phi \to M=N$$