rinvmod

Description: Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo . (Contributed by AV, 31-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rinvmod.b	$⊢ B = {Base}_{G}$
2		rinvmod.0	$⊢ \underset{˙}{0} = 0_{G}$
3		rinvmod.p	$⊢ \underset{˙}{+} = +_{G}$
4		rinvmod.m	$⊢ φ \to G \in CMnd$
5		rinvmod.a	$⊢ φ \to A \in B$
6	4	adantr	$⊢ (φ \land w \in B) \to G \in CMnd$
7		simpr	$⊢ (φ \land w \in B) \to w \in B$
8	5	adantr	$⊢ (φ \land w \in B) \to A \in B$
9	1 3	cmncom	$⊢ (G \in CMnd \land w \in B \land A \in B) \to w \underset{˙}{+} A = A \underset{˙}{+} w$
10	6 7 8 9	syl3anc	$⊢ (φ \land w \in B) \to w \underset{˙}{+} A = A \underset{˙}{+} w$
11	10	adantr	$⊢ ((φ \land w \in B) \land A \underset{˙}{+} w = \underset{˙}{0}) \to w \underset{˙}{+} A = A \underset{˙}{+} w$
12		simpr	$⊢ ((φ \land w \in B) \land A \underset{˙}{+} w = \underset{˙}{0}) \to A \underset{˙}{+} w = \underset{˙}{0}$
13	11 12	eqtrd	$⊢ ((φ \land w \in B) \land A \underset{˙}{+} w = \underset{˙}{0}) \to w \underset{˙}{+} A = \underset{˙}{0}$
14	13 12	jca	$⊢ ((φ \land w \in B) \land A \underset{˙}{+} w = \underset{˙}{0}) \to (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0})$
15	14	ex	$⊢ (φ \land w \in B) \to (A \underset{˙}{+} w = \underset{˙}{0} \to (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}))$
16	15	ralrimiva	$⊢ φ \to \forall w \in B (A \underset{˙}{+} w = \underset{˙}{0} \to (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}))$
17		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
18	4 17	syl	$⊢ φ \to G \in Mnd$
19	1 2 3 18 5	mndinvmod	$⊢ φ \to \exists^{*} w \in B (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0})$
20		rmoim	$⊢ \forall w \in B (A \underset{˙}{+} w = \underset{˙}{0} \to (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0})) \to (\exists^{} w \in B (w \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} w = \underset{˙}{0}) \to \exists^{} w \in B A \underset{˙}{+} w = \underset{˙}{0})$
21	16 19 20	sylc	$⊢ φ \to \exists^{*} w \in B A \underset{˙}{+} w = \underset{˙}{0}$

Metamath Proof Explorer

Theorem rinvmod

Proof