Theorem 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={\mathrm{Base}}_G$$
	mndinvmod.0	$$⊢\underset{\dot{}}{0}=0_G$$
	mndinvmod.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mndinvmod.m	$$⊢\phi \to G\in \mathrm{Mnd}$$
	mndinvmod.a	$$⊢\phi \to A\in B$$
Assertion	mndinvmod	$$⊢\phi \to {\exists }^{*}w\in B\left(w\underset{\dot{}}{+}A=\underset{\dot{}}{0}\wedge A\underset{\dot{}}{+}w=\underset{\dot{}}{0}\right)$$

Proof

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