mndinvmod

Description: Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024)

	Ref	Expression
Hypotheses	mndinvmod.b	$⊢ B = {Base}_{G}$
	mndinvmod.0	$⊢ \underset{˙}{0} = 0_{G}$
	mndinvmod.p	$⊢ \underset{˙}{+} = +_{G}$
	mndinvmod.m	$⊢ φ \to G \in Mnd$
	mndinvmod.a	$⊢ φ \to A \in B$
Assertion	mndinvmod	$⊢ φ \to \exists^{*} w \in B (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		mndinvmod.b	$⊢ B = {Base}_{G}$
2		mndinvmod.0	$⊢ \underset{˙}{0} = 0_{G}$
3		mndinvmod.p	$⊢ \underset{˙}{+} = +_{G}$
4		mndinvmod.m	$⊢ φ \to G \in Mnd$
5		mndinvmod.a	$⊢ φ \to A \in B$
6		simpl	$⊢ (w \in B \land v \in B) \to w \in B$
7	1 3 2	mndrid	$⊢ (G \in Mnd \land w \in B) \to w \underset{˙}{+} \underset{˙}{0} = w$
8	4 6 7	syl2an	$⊢ (φ \land (w \in B \land v \in B)) \to w \underset{˙}{+} \underset{˙}{0} = w$
9	8	eqcomd	$⊢ (φ \land (w \in B \land v \in B)) \to w = w \underset{˙}{+} \underset{˙}{0}$
10	9	adantr	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to w = w \underset{˙}{+} \underset{˙}{0}$
11		oveq2	$⊢ \underset{˙}{0} = A \underset{˙}{+} v \to w \underset{˙}{+} \underset{˙}{0} = w \underset{˙}{+} (A \underset{˙}{+} v)$
12	11	eqcoms	$⊢ A \underset{˙}{+} v = \underset{˙}{0} \to w \underset{˙}{+} \underset{˙}{0} = w \underset{˙}{+} (A \underset{˙}{+} v)$
13	12	adantl	$⊢ (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}) \to w \underset{˙}{+} \underset{˙}{0} = w \underset{˙}{+} (A \underset{˙}{+} v)$
14	13	adantl	$⊢ ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0})) \to w \underset{˙}{+} \underset{˙}{0} = w \underset{˙}{+} (A \underset{˙}{+} v)$
15	14	adantl	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to w \underset{˙}{+} \underset{˙}{0} = w \underset{˙}{+} (A \underset{˙}{+} v)$
16	4	adantr	$⊢ (φ \land (w \in B \land v \in B)) \to G \in Mnd$
17	6	adantl	$⊢ (φ \land (w \in B \land v \in B)) \to w \in B$
18	5	adantr	$⊢ (φ \land (w \in B \land v \in B)) \to A \in B$
19		simpr	$⊢ (w \in B \land v \in B) \to v \in B$
20	19	adantl	$⊢ (φ \land (w \in B \land v \in B)) \to v \in B$
21	1 3	mndass	$⊢ (G \in Mnd \land (w \in B \land A \in B \land v \in B)) \to (w \underset{˙}{+} A) \underset{˙}{+} v = w \underset{˙}{+} (A \underset{˙}{+} v)$
22	21	eqcomd	$⊢ (G \in Mnd \land (w \in B \land A \in B \land v \in B)) \to w \underset{˙}{+} (A \underset{˙}{+} v) = (w \underset{˙}{+} A) \underset{˙}{+} v$
23	16 17 18 20 22	syl13anc	$⊢ (φ \land (w \in B \land v \in B)) \to w \underset{˙}{+} (A \underset{˙}{+} v) = (w \underset{˙}{+} A) \underset{˙}{+} v$
24	23	adantr	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to w \underset{˙}{+} (A \underset{˙}{+} v) = (w \underset{˙}{+} A) \underset{˙}{+} v$
25		oveq1	$⊢ w \underset{˙}{+} A = \underset{˙}{0} \to (w \underset{˙}{+} A) \underset{˙}{+} v = \underset{˙}{0} \underset{˙}{+} v$
26	25	adantr	$⊢ (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \to (w \underset{˙}{+} A) \underset{˙}{+} v = \underset{˙}{0} \underset{˙}{+} v$
27	26	adantr	$⊢ ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0})) \to (w \underset{˙}{+} A) \underset{˙}{+} v = \underset{˙}{0} \underset{˙}{+} v$
28	27	adantl	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to (w \underset{˙}{+} A) \underset{˙}{+} v = \underset{˙}{0} \underset{˙}{+} v$
29	1 3 2	mndlid	$⊢ (G \in Mnd \land v \in B) \to \underset{˙}{0} \underset{˙}{+} v = v$
30	4 19 29	syl2an	$⊢ (φ \land (w \in B \land v \in B)) \to \underset{˙}{0} \underset{˙}{+} v = v$
31	30	adantr	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to \underset{˙}{0} \underset{˙}{+} v = v$
32	24 28 31	3eqtrd	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to w \underset{˙}{+} (A \underset{˙}{+} v) = v$
33	10 15 32	3eqtrd	$⊢ ((φ \land (w \in B \land v \in B)) \land ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))) \to w = v$
34	33	ex	$⊢ (φ \land (w \in B \land v \in B)) \to (((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0})) \to w = v)$
35	34	ralrimivva	$⊢ φ \to \forall w \in B \forall v \in B (((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0})) \to w = v)$
36		oveq1	$⊢ w = v \to w \underset{˙}{+} A = v \underset{˙}{+} A$
37	36	eqeq1d	$⊢ w = v \to (w \underset{˙}{+} A = \underset{˙}{0} \leftrightarrow v \underset{˙}{+} A = \underset{˙}{0})$
38		oveq2	$⊢ w = v \to A \underset{˙}{+} w = A \underset{˙}{+} v$
39	38	eqeq1d	$⊢ w = v \to (A \underset{˙}{+} w = \underset{˙}{0} \leftrightarrow A \underset{˙}{+} v = \underset{˙}{0})$
40	37 39	anbi12d	$⊢ w = v \to ((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \leftrightarrow (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0}))$
41	40	rmo4	$⊢ \exists^{*} w \in B (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \leftrightarrow \forall w \in B \forall v \in B (((w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \land (v \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} v = \underset{˙}{0})) \to w = v)$
42	35 41	sylibr	$⊢ φ \to \exists^{*} w \in B (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0})$

Metamath Proof Explorer

Theorem mndinvmod

Proof