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	$⊢ \underset{˙}{0} = 0_{E}$
		mndlrinv.p	$⊢ \underset{˙}{+} = +_{E}$
		mndlrinv.e	$⊢ φ \to E \in Mnd$
		mndlrinv.x	$⊢ φ \to X \in B$
		mndlrinv.m	$⊢ φ \to M \in B$
		mndlrinv.n	$⊢ φ \to N \in B$
		mndlrinv.1	$⊢ φ \to M \underset{˙}{+} X = \underset{˙}{0}$
		mndlrinv.2	$⊢ φ \to X \underset{˙}{+} N = \underset{˙}{0}$
	Assertion	mndlrinv	$⊢ φ \to M = N$

Proof

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