addsrmo

Description: There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019)

		Ref	Expression
	Assertion	addsrmo	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \exists^{*} z \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})$

Proof

Step	Hyp	Ref	Expression
1		enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$
2	1	a1i	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ~_{𝑹} Er (𝑷 \times 𝑷)$
3		prsrlem1	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ((((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \land ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))) \land (w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g))$
4		addcmpblnr	$⊢ (((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \land ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))) \to ((w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g) \to ⟨w +_{𝑷} u, v +_{𝑷} t⟩ ~_{𝑹} ⟨s +_{𝑷} g, f +_{𝑷} h⟩)$
5	4	imp	$⊢ ((((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \land ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))) \land (w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g)) \to ⟨w +_{𝑷} u, v +_{𝑷} t⟩ ~_{𝑹} ⟨s +_{𝑷} g, f +_{𝑷} h⟩$
6	3 5	syl	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨w +_{𝑷} u, v +_{𝑷} t⟩ ~_{𝑹} ⟨s +_{𝑷} g, f +_{𝑷} h⟩$
7	2 6	erthi	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}$
8	7	adantrlr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}$
9	8	adantrrr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}))) \to [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}$
10		simprlr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}))) \to z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}$
11		simprrr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}))) \to q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}$
12	9 10 11	3eqtr4d	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}))) \to z = q$
13	12	expr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to (((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}) \to z = q)$
14	13	exlimdvv	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to (\exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}) \to z = q)$
15	14	exlimdvv	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}) \to z = q)$
16	15	ex	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}) \to z = q))$
17	16	exlimdvv	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (\exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}) \to z = q))$
18	17	exlimdvv	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}) \to z = q))$
19	18	impd	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹})) \to z = q)$
20	19	alrimivv	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹})) \to z = q)$
21		opeq12	$⊢ (w = s \land v = f) \to ⟨w, v⟩ = ⟨s, f⟩$
22	21	eceq1d	$⊢ (w = s \land v = f) \to [⟨w, v⟩] ~_{𝑹} = [⟨s, f⟩] ~_{𝑹}$
23	22	eqeq2d	$⊢ (w = s \land v = f) \to (A = [⟨w, v⟩] ~_{𝑹} \leftrightarrow A = [⟨s, f⟩] ~_{𝑹})$
24	23	anbi1d	$⊢ (w = s \land v = f) \to ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \leftrightarrow (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}))$
25		simpl	$⊢ (w = s \land v = f) \to w = s$
26	25	oveq1d	$⊢ (w = s \land v = f) \to w +_{𝑷} u = s +_{𝑷} u$
27		simpr	$⊢ (w = s \land v = f) \to v = f$
28	27	oveq1d	$⊢ (w = s \land v = f) \to v +_{𝑷} t = f +_{𝑷} t$
29	26 28	opeq12d	$⊢ (w = s \land v = f) \to ⟨w +_{𝑷} u, v +_{𝑷} t⟩ = ⟨s +_{𝑷} u, f +_{𝑷} t⟩$
30	29	eceq1d	$⊢ (w = s \land v = f) \to [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} = [⟨s +_{𝑷} u, f +_{𝑷} t⟩] ~_{𝑹}$
31	30	eqeq2d	$⊢ (w = s \land v = f) \to (q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} \leftrightarrow q = [⟨s +_{𝑷} u, f +_{𝑷} t⟩] ~_{𝑹})$
32	24 31	anbi12d	$⊢ (w = s \land v = f) \to (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} u, f +_{𝑷} t⟩] ~_{𝑹}))$
33		opeq12	$⊢ (u = g \land t = h) \to ⟨u, t⟩ = ⟨g, h⟩$
34	33	eceq1d	$⊢ (u = g \land t = h) \to [⟨u, t⟩] ~_{𝑹} = [⟨g, h⟩] ~_{𝑹}$
35	34	eqeq2d	$⊢ (u = g \land t = h) \to (B = [⟨u, t⟩] ~_{𝑹} \leftrightarrow B = [⟨g, h⟩] ~_{𝑹})$
36	35	anbi2d	$⊢ (u = g \land t = h) \to ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \leftrightarrow (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))$
37		simpl	$⊢ (u = g \land t = h) \to u = g$
38	37	oveq2d	$⊢ (u = g \land t = h) \to s +_{𝑷} u = s +_{𝑷} g$
39		simpr	$⊢ (u = g \land t = h) \to t = h$
40	39	oveq2d	$⊢ (u = g \land t = h) \to f +_{𝑷} t = f +_{𝑷} h$
41	38 40	opeq12d	$⊢ (u = g \land t = h) \to ⟨s +_{𝑷} u, f +_{𝑷} t⟩ = ⟨s +_{𝑷} g, f +_{𝑷} h⟩$
42	41	eceq1d	$⊢ (u = g \land t = h) \to [⟨s +_{𝑷} u, f +_{𝑷} t⟩] ~_{𝑹} = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}$
43	42	eqeq2d	$⊢ (u = g \land t = h) \to (q = [⟨s +_{𝑷} u, f +_{𝑷} t⟩] ~_{𝑹} \leftrightarrow q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹})$
44	36 43	anbi12d	$⊢ (u = g \land t = h) \to (((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} u, f +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}))$
45	32 44	cbvex4vw	$⊢ \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹})$
46	45	anbi2i	$⊢ (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \leftrightarrow (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹}))$
47	46	imbi1i	$⊢ ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to z = q) \leftrightarrow ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹})) \to z = q)$
48	47	2albii	$⊢ \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to z = q) \leftrightarrow \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨s +_{𝑷} g, f +_{𝑷} h⟩] ~_{𝑹})) \to z = q)$
49	20 48	sylibr	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to z = q)$
50		eqeq1	$⊢ z = q \to (z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} \leftrightarrow q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})$
51	50	anbi2d	$⊢ z = q \to (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
52	51	4exbidv	$⊢ z = q \to (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
53	52	mo4	$⊢ \exists^{*} z \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \to z = q)$
54	49 53	sylibr	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \exists^{*} z \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})$

Metamath Proof Explorer

Theorem addsrmo

Proof