addsrpr

Description: Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

		Ref	Expression
	Assertion	addsrpr	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to [⟨A, B⟩] ~_{𝑹} +_{𝑹} [⟨C, D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ⟨A, B⟩ \in (𝑷 \times 𝑷)$
2		enrex	$⊢ ~_{𝑹} \in V$
3	2	ecelqsi	$⊢ ⟨A, B⟩ \in (𝑷 \times 𝑷) \to [⟨A, B⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
4	1 3	syl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to [⟨A, B⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
5		opelxpi	$⊢ (C \in 𝑷 \land D \in 𝑷) \to ⟨C, D⟩ \in (𝑷 \times 𝑷)$
6	2	ecelqsi	$⊢ ⟨C, D⟩ \in (𝑷 \times 𝑷) \to [⟨C, D⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
7	5 6	syl	$⊢ (C \in 𝑷 \land D \in 𝑷) \to [⟨C, D⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
8	4 7	anim12i	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ([⟨A, B⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land [⟨C, D⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}))$
9		eqid	$⊢ [⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹}$
10		eqid	$⊢ [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}$
11	9 10	pm3.2i	$⊢ ([⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹})$
12		eqid	$⊢ [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}$
13		opeq12	$⊢ (w = A \land v = B) \to ⟨w, v⟩ = ⟨A, B⟩$
14	13	eceq1d	$⊢ (w = A \land v = B) \to [⟨w, v⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹}$
15	14	eqeq2d	$⊢ (w = A \land v = B) \to ([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \leftrightarrow [⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹})$
16	15	anbi1d	$⊢ (w = A \land v = B) \to (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \leftrightarrow ([⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}))$
17		simpl	$⊢ (w = A \land v = B) \to w = A$
18	17	oveq1d	$⊢ (w = A \land v = B) \to w +_{𝑷} C = A +_{𝑷} C$
19		simpr	$⊢ (w = A \land v = B) \to v = B$
20	19	oveq1d	$⊢ (w = A \land v = B) \to v +_{𝑷} D = B +_{𝑷} D$
21	18 20	opeq12d	$⊢ (w = A \land v = B) \to ⟨w +_{𝑷} C, v +_{𝑷} D⟩ = ⟨A +_{𝑷} C, B +_{𝑷} D⟩$
22	21	eceq1d	$⊢ (w = A \land v = B) \to [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}$
23	22	eqeq2d	$⊢ (w = A \land v = B) \to ([⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹} \leftrightarrow [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹})$
24	16 23	anbi12d	$⊢ (w = A \land v = B) \to ((([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹}) \leftrightarrow (([⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}))$
25	24	spc2egv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((([⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to \exists w \exists v (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹}))$
26		opeq12	$⊢ (u = C \land t = D) \to ⟨u, t⟩ = ⟨C, D⟩$
27	26	eceq1d	$⊢ (u = C \land t = D) \to [⟨u, t⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}$
28	27	eqeq2d	$⊢ (u = C \land t = D) \to ([⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹} \leftrightarrow [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹})$
29	28	anbi2d	$⊢ (u = C \land t = D) \to (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \leftrightarrow ([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}))$
30		simpl	$⊢ (u = C \land t = D) \to u = C$
31	30	oveq2d	$⊢ (u = C \land t = D) \to w +_{𝑷} u = w +_{𝑷} C$
32		simpr	$⊢ (u = C \land t = D) \to t = D$
33	32	oveq2d	$⊢ (u = C \land t = D) \to v +_{𝑷} t = v +_{𝑷} D$
34	31 33	opeq12d	$⊢ (u = C \land t = D) \to ⟨w +_{𝑷} u, v +_{𝑷} t⟩ = ⟨w +_{𝑷} C, v +_{𝑷} D⟩$
35	34	eceq1d	$⊢ (u = C \land t = D) \to [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹}$
36	35	eqeq2d	$⊢ (u = C \land t = D) \to ([⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} \leftrightarrow [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹})$
37	29 36	anbi12d	$⊢ (u = C \land t = D) \to ((([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹}))$
38	37	spc2egv	$⊢ (C \in 𝑷 \land D \in 𝑷) \to ((([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹}) \to \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
39	38	2eximdv	$⊢ (C \in 𝑷 \land D \in 𝑷) \to (\exists w \exists v (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} C, v +_{𝑷} D⟩] ~_{𝑹}) \to \exists w \exists v \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
40	25 39	sylan9	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ((([⟨A, B⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to \exists w \exists v \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
41	11 12 40	mp2ani	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to \exists w \exists v \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})$
42		ecexg	$⊢ ~_{𝑹} \in V \to [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} \in V$
43	2 42	ax-mp	$⊢ [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} \in V$
44		simp1	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to x = [⟨A, B⟩] ~_{𝑹}$
45	44	eqeq1d	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to (x = [⟨w, v⟩] ~_{𝑹} \leftrightarrow [⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹})$
46		simp2	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to y = [⟨C, D⟩] ~_{𝑹}$
47	46	eqeq1d	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to (y = [⟨u, t⟩] ~_{𝑹} \leftrightarrow [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹})$
48	45 47	anbi12d	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \leftrightarrow ([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}))$
49		simp3	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}$
50	49	eqeq1d	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to (z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹} \leftrightarrow [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})$
51	48 50	anbi12d	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to (((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
52	51	4exbidv	$⊢ (x = [⟨A, B⟩] ~_{𝑹} \land y = [⟨C, D⟩] ~_{𝑹} \land z = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}) \to (\exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \leftrightarrow \exists w \exists v \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
53		addsrmo	$⊢ (x \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land y \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \exists^{*} z \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})$
54		df-plr	$⊢ +_{𝑹} = \{⟨⟨x, y⟩, z⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))\}$
55		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
56	55	eleq2i	$⊢ x \in 𝑹 \leftrightarrow x \in ((𝑷 \times 𝑷) / ~_{𝑹})$
57	55	eleq2i	$⊢ y \in 𝑹 \leftrightarrow y \in ((𝑷 \times 𝑷) / ~_{𝑹})$
58	56 57	anbi12i	$⊢ (x \in 𝑹 \land y \in 𝑹) \leftrightarrow (x \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land y \in ((𝑷 \times 𝑷) / ~_{𝑹}))$
59	58	anbi1i	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹})) \leftrightarrow ((x \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land y \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))$
60	59	oprabbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land y \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))\}$
61	54 60	eqtri	$⊢ +_{𝑹} = \{⟨⟨x, y⟩, z⟩ \| ((x \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land y \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land \exists w \exists v \exists u \exists t ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}))\}$
62	52 53 61	ovig	$⊢ ([⟨A, B⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land [⟨C, D⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} \in V) \to (\exists w \exists v \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \to [⟨A, B⟩] ~_{𝑹} +_{𝑹} [⟨C, D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹})$
63	43 62	mp3an3	$⊢ ([⟨A, B⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land [⟨C, D⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (\exists w \exists v \exists u \exists t (([⟨A, B⟩] ~_{𝑹} = [⟨w, v⟩] ~_{𝑹} \land [⟨C, D⟩] ~_{𝑹} = [⟨u, t⟩] ~_{𝑹}) \land [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹} = [⟨w +_{𝑷} u, v +_{𝑷} t⟩] ~_{𝑹}) \to [⟨A, B⟩] ~_{𝑹} +_{𝑹} [⟨C, D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹})$
64	8 41 63	sylc	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to [⟨A, B⟩] ~_{𝑹} +_{𝑹} [⟨C, D⟩] ~_{𝑹} = [⟨A +_{𝑷} C, B +_{𝑷} D⟩] ~_{𝑹}$

Metamath Proof Explorer

Theorem addsrpr

Proof