Theorem 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={\mathrm{Base}}_G$$
	rinvmod.0	$$⊢\underset{\dot{}}{0}=0_G$$
	rinvmod.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	rinvmod.m	$$⊢\phi \to G\in \mathrm{CMnd}$$
	rinvmod.a	$$⊢\phi \to A\in B$$
Assertion	rinvmod	$$⊢\phi \to {\exists }^{*}w\in BA\underset{\dot{}}{+}w=\underset{\dot{}}{0}$$

Proof

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