mndlrinvb

Description: In a monoid, if an element has both a left-inverse and a right-inverse, 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$
Assertion	mndlrinvb	$⊢ φ \to ((\exists u \in B X \underset{˙}{+} u = \underset{˙}{0} \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0}))$

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		oveq2	$⊢ z = u \to X \underset{˙}{+} z = X \underset{˙}{+} u$
7	6	eqeq1d	$⊢ z = u \to (X \underset{˙}{+} z = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} u = \underset{˙}{0})$
8		oveq1	$⊢ z = u \to z \underset{˙}{+} X = u \underset{˙}{+} X$
9	8	eqeq1d	$⊢ z = u \to (z \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow u \underset{˙}{+} X = \underset{˙}{0})$
10	7 9	anbi12d	$⊢ z = u \to ((X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow (X \underset{˙}{+} u = \underset{˙}{0} \land u \underset{˙}{+} X = \underset{˙}{0}))$
11		simplr	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to u \in B$
12		simpr	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to X \underset{˙}{+} u = \underset{˙}{0}$
13	4	ad4antr	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to E \in Mnd$
14	5	ad4antr	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to X \in B$
15		simpllr	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v \in B$
16		simp-4r	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v \underset{˙}{+} X = \underset{˙}{0}$
17	1 2 3 13 14 15 11 16 12	mndlrinv	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v = u$
18	17	oveq1d	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v \underset{˙}{+} X = u \underset{˙}{+} X$
19	18 16	eqtr3d	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to u \underset{˙}{+} X = \underset{˙}{0}$
20	12 19	jca	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to (X \underset{˙}{+} u = \underset{˙}{0} \land u \underset{˙}{+} X = \underset{˙}{0})$
21	10 11 20	rspcedvdw	$⊢ ((((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})$
22	21	r19.29an	$⊢ (((φ \land v \underset{˙}{+} X = \underset{˙}{0}) \land v \in B) \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}) \to \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})$
23	22	an42ds	$⊢ (((φ \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})$
24	23	r19.29an	$⊢ ((φ \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}) \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}) \to \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})$
25	24	anasss	$⊢ (φ \land (\exists u \in B X \underset{˙}{+} u = \underset{˙}{0} \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0})) \to \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})$
26		oveq2	$⊢ u = z \to X \underset{˙}{+} u = X \underset{˙}{+} z$
27	26	eqeq1d	$⊢ u = z \to (X \underset{˙}{+} u = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} z = \underset{˙}{0})$
28		simplr	$⊢ ((φ \land z \in B) \land (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to z \in B$
29		simprl	$⊢ ((φ \land z \in B) \land (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to X \underset{˙}{+} z = \underset{˙}{0}$
30	27 28 29	rspcedvdw	$⊢ ((φ \land z \in B) \land (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}$
31		oveq1	$⊢ v = z \to v \underset{˙}{+} X = z \underset{˙}{+} X$
32	31	eqeq1d	$⊢ v = z \to (v \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow z \underset{˙}{+} X = \underset{˙}{0})$
33		simprr	$⊢ ((φ \land z \in B) \land (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to z \underset{˙}{+} X = \underset{˙}{0}$
34	32 28 33	rspcedvdw	$⊢ ((φ \land z \in B) \land (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}$
35	30 34	jca	$⊢ ((φ \land z \in B) \land (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to (\exists u \in B X \underset{˙}{+} u = \underset{˙}{0} \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0})$
36	35	r19.29an	$⊢ (φ \land \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})) \to (\exists u \in B X \underset{˙}{+} u = \underset{˙}{0} \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0})$
37	25 36	impbida	$⊢ φ \to ((\exists u \in B X \underset{˙}{+} u = \underset{˙}{0} \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}))$
38		oveq2	$⊢ y = z \to X \underset{˙}{+} y = X \underset{˙}{+} z$
39	38	eqeq1d	$⊢ y = z \to (X \underset{˙}{+} y = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} z = \underset{˙}{0})$
40		oveq1	$⊢ y = z \to y \underset{˙}{+} X = z \underset{˙}{+} X$
41	40	eqeq1d	$⊢ y = z \to (y \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow z \underset{˙}{+} X = \underset{˙}{0})$
42	39 41	anbi12d	$⊢ y = z \to ((X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}))$
43	42	cbvrexvw	$⊢ \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow \exists z \in B (X \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0})$
44	37 43	bitr4di	$⊢ φ \to ((\exists u \in B X \underset{˙}{+} u = \underset{˙}{0} \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem mndlrinvb

Proof