mndmolinv

Description: An element of a monoid that has a right inverse has at most one left inverse. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	mndmolinv.1	$⊢ B = {Base}_{M}$
	mndmolinv.2	$⊢ φ \to M \in Mnd$
	mndmolinv.3	$⊢ φ \to A \in B$
	mndmolinv.4	$⊢ φ \to \exists x \in B A +_{M} x = 0_{M}$
Assertion	mndmolinv	$⊢ φ \to \exists^{*} x \in B x +_{M} A = 0_{M}$

Proof

Step	Hyp	Ref	Expression
1		mndmolinv.1	$⊢ B = {Base}_{M}$
2		mndmolinv.2	$⊢ φ \to M \in Mnd$
3		mndmolinv.3	$⊢ φ \to A \in B$
4		mndmolinv.4	$⊢ φ \to \exists x \in B A +_{M} x = 0_{M}$
5		nfv	$⊢ Ⅎ y A +_{M} x = 0_{M}$
6		nfv	$⊢ Ⅎ x A +_{M} y = 0_{M}$
7		oveq2	$⊢ x = y \to A +_{M} x = A +_{M} y$
8	7	eqeq1d	$⊢ x = y \to (A +_{M} x = 0_{M} \leftrightarrow A +_{M} y = 0_{M})$
9	5 6 8	cbvrexw	$⊢ \exists x \in B A +_{M} x = 0_{M} \leftrightarrow \exists y \in B A +_{M} y = 0_{M}$
10	9	biimpi	$⊢ \exists x \in B A +_{M} x = 0_{M} \to \exists y \in B A +_{M} y = 0_{M}$
11	4 10	syl	$⊢ φ \to \exists y \in B A +_{M} y = 0_{M}$
12	2	ad4antr	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to M \in Mnd$
13		simplr	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x \in B$
14		eqid	$⊢ +_{M} = +_{M}$
15		eqid	$⊢ 0_{M} = 0_{M}$
16	1 14 15	mndrid	$⊢ (M \in Mnd \land x \in B) \to x +_{M} 0_{M} = x$
17	12 13 16	syl2anc	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x +_{M} 0_{M} = x$
18	17	eqcomd	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x = x +_{M} 0_{M}$
19		simpllr	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to A +_{M} y = 0_{M}$
20	19	eqcomd	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to 0_{M} = A +_{M} y$
21	20	oveq2d	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x +_{M} 0_{M} = x +_{M} (A +_{M} y)$
22	18 21	eqtrd	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x = x +_{M} (A +_{M} y)$
23	3	ad4antr	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to A \in B$
24		simp-4r	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to y \in B$
25	13 23 24	3jca	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to (x \in B \land A \in B \land y \in B)$
26	1 14	mndass	$⊢ (M \in Mnd \land (x \in B \land A \in B \land y \in B)) \to (x +_{M} A) +_{M} y = x +_{M} (A +_{M} y)$
27	12 25 26	syl2anc	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to (x +_{M} A) +_{M} y = x +_{M} (A +_{M} y)$
28	27	eqcomd	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x +_{M} (A +_{M} y) = (x +_{M} A) +_{M} y$
29		simpr	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x +_{M} A = 0_{M}$
30	29	oveq1d	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to (x +_{M} A) +_{M} y = 0_{M} +_{M} y$
31	1 14 15	mndlid	$⊢ (M \in Mnd \land y \in B) \to 0_{M} +_{M} y = y$
32	12 24 31	syl2anc	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to 0_{M} +_{M} y = y$
33	30 32	eqtrd	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to (x +_{M} A) +_{M} y = y$
34	22 28 33	3eqtrd	$⊢ ((((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \land x +_{M} A = 0_{M}) \to x = y$
35	34	ex	$⊢ (((φ \land y \in B) \land A +_{M} y = 0_{M}) \land x \in B) \to (x +_{M} A = 0_{M} \to x = y)$
36	35	ralrimiva	$⊢ ((φ \land y \in B) \land A +_{M} y = 0_{M}) \to \forall x \in B (x +_{M} A = 0_{M} \to x = y)$
37	36	ex	$⊢ (φ \land y \in B) \to (A +_{M} y = 0_{M} \to \forall x \in B (x +_{M} A = 0_{M} \to x = y))$
38	37	reximdva	$⊢ φ \to (\exists y \in B A +_{M} y = 0_{M} \to \exists y \in B \forall x \in B (x +_{M} A = 0_{M} \to x = y))$
39	11 38	mpd	$⊢ φ \to \exists y \in B \forall x \in B (x +_{M} A = 0_{M} \to x = y)$
40		nfv	$⊢ Ⅎ y x +_{M} A = 0_{M}$
41	40	rmo2i	$⊢ \exists y \in B \forall x \in B (x +_{M} A = 0_{M} \to x = y) \to \exists^{*} x \in B x +_{M} A = 0_{M}$
42	39 41	syl	$⊢ φ \to \exists^{*} x \in B x +_{M} A = 0_{M}$

Metamath Proof Explorer

Theorem mndmolinv

Proof