Theorem addsrpr 7648

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

Assertion

Ref	Expression
addsrpr	⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )

Proof of Theorem addsrpr

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opelxpi 4615	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ⟨𝐴, 𝐵⟩ ∈ (P × P))
2		enrex 7640	. . . . 5 ⊢ ~R ∈ V
3	2	ecelqsi 6527	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ (P × P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
4	1, 3	syl 14	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
5		opelxpi 4615	. . . 4 ⊢ ((𝐶 ∈ P ∧ 𝐷 ∈ P) → ⟨𝐶, 𝐷⟩ ∈ (P × P))
6	2	ecelqsi 6527	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ ∈ (P × P) → [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ))
7	5, 6	syl 14	. . 3 ⊢ ((𝐶 ∈ P ∧ 𝐷 ∈ P) → [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ))
8	4, 7	anim12i 336	. 2 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R )))
9		eqid 2157	. . . 4 ⊢ [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R
10		eqid 2157	. . . 4 ⊢ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R
11	9, 10	pm3.2i 270	. . 3 ⊢ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
12		eqid 2157	. . 3 ⊢ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R
13		opeq12 3743	. . . . . . . . 9 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ⟨𝑤, 𝑣⟩ = ⟨𝐴, 𝐵⟩)
14	13	eceq1d 6509	. . . . . . . 8 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → [⟨𝑤, 𝑣⟩] ~R = [⟨𝐴, 𝐵⟩] ~R )
15	14	eqeq2d 2169	. . . . . . 7 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ))
16	15	anbi1d 461	. . . . . 6 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
17		simpl 108	. . . . . . . . . 10 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 𝑤 = 𝐴)
18	17	oveq1d 5833	. . . . . . . . 9 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑤 +P 𝐶) = (𝐴 +P 𝐶))
19		simpr 109	. . . . . . . . . 10 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
20	19	oveq1d 5833	. . . . . . . . 9 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑣 +P 𝐷) = (𝐵 +P 𝐷))
21	18, 20	opeq12d 3749	. . . . . . . 8 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩ = ⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩)
22	21	eceq1d 6509	. . . . . . 7 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
23	22	eqeq2d 2169	. . . . . 6 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ([⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
24	16, 23	anbi12d 465	. . . . 5 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )))
25	24	spc2egv 2802	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ∃𝑤∃𝑣(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )))
26		opeq12 3743	. . . . . . . . . 10 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ⟨𝑢, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
27	26	eceq1d 6509	. . . . . . . . 9 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → [⟨𝑢, 𝑡⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
28	27	eqeq2d 2169	. . . . . . . 8 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ([⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ))
29	28	anbi2d 460	. . . . . . 7 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
30		simpl 108	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 𝑢 = 𝐶)
31	30	oveq2d 5834	. . . . . . . . . 10 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑤 +P 𝑢) = (𝑤 +P 𝐶))
32		simpr 109	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 𝑡 = 𝐷)
33	32	oveq2d 5834	. . . . . . . . . 10 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑣 +P 𝑡) = (𝑣 +P 𝐷))
34	31, 33	opeq12d 3749	. . . . . . . . 9 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩ = ⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩)
35	34	eceq1d 6509	. . . . . . . 8 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )
36	35	eqeq2d 2169	. . . . . . 7 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ([⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ))
37	29, 36	anbi12d 465	. . . . . 6 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )))
38	37	spc2egv 2802	. . . . 5 ⊢ ((𝐶 ∈ P ∧ 𝐷 ∈ P) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) → ∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
39	38	2eximdv 1862	. . . 4 ⊢ ((𝐶 ∈ P ∧ 𝐷 ∈ P) → (∃𝑤∃𝑣(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) → ∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
40	25, 39	sylan9 407	. . 3 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
41	11, 12, 40	mp2ani 429	. 2 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
42		ecexg 6477	. . . 4 ⊢ ( ~R ∈ V → [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V)
43	2, 42	ax-mp 5	. . 3 ⊢ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V
44		simp1 982	. . . . . . . 8 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑥 = [⟨𝐴, 𝐵⟩] ~R )
45	44	eqeq1d 2166	. . . . . . 7 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑥 = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ))
46		simp2 983	. . . . . . . 8 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑦 = [⟨𝐶, 𝐷⟩] ~R )
47	46	eqeq1d 2166	. . . . . . 7 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑦 = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ))
48	45, 47	anbi12d 465	. . . . . 6 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R )))
49		simp3 984	. . . . . . 7 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
50	49	eqeq1d 2166	. . . . . 6 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
51	48, 50	anbi12d 465	. . . . 5 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
52	51	4exbidv 1850	. . . 4 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ ∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
53		addsrmo 7646	. . . 4 ⊢ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
54		df-plr 7631	. . . . 5 ⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
55		df-nr 7630	. . . . . . . . 9 ⊢ R = ((P × P) / ~R )
56	55	eleq2i 2224	. . . . . . . 8 ⊢ (𝑥 ∈ R ↔ 𝑥 ∈ ((P × P) / ~R ))
57	55	eleq2i 2224	. . . . . . . 8 ⊢ (𝑦 ∈ R ↔ 𝑦 ∈ ((P × P) / ~R ))
58	56, 57	anbi12i 456	. . . . . . 7 ⊢ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ↔ (𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )))
59	58	anbi1i 454	. . . . . 6 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )) ↔ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
60	59	oprabbii 5870	. . . . 5 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
61	54, 60	eqtri 2178	. . . 4 ⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
62	52, 53, 61	ovig 5936	. . 3 ⊢ (([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V) → (∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
63	43, 62	mp3an3 1308	. 2 ⊢ (([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R )) → (∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
64	8, 41, 63	sylc 62	1 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963   = wceq 1335  ∃wex 1472   ∈ wcel 2128  Vcvv 2712  ⟨cop 3563   × cxp 4581  (class class class)co 5818  {coprab 5819  [cec 6471   / cqs 6472  Pcnp 7194   +_P cpp 7196   ~_R cer 7199  Rcnr 7200   +_R cplr 7204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-eprel 4248  df-id 4252  df-po 4255  df-iso 4256  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-recs 6246  df-irdg 6311  df-1o 6357  df-2o 6358  df-oadd 6361  df-omul 6362  df-er 6473  df-ec 6475  df-qs 6479  df-ni 7207  df-pli 7208  df-mi 7209  df-lti 7210  df-plpq 7247  df-mpq 7248  df-enq 7250  df-nqqs 7251  df-plqqs 7252  df-mqqs 7253  df-1nqqs 7254  df-rq 7255  df-ltnqqs 7256  df-enq0 7327  df-nq0 7328  df-0nq0 7329  df-plq0 7330  df-mq0 7331  df-inp 7369  df-iplp 7371  df-enr 7629  df-nr 7630  df-plr 7631

This theorem is referenced by:  addclsr  7656  addcomsrg  7658  addasssrg  7659  distrsrg  7662  m1p1sr  7663  0idsr  7670  ltasrg  7673  prsradd  7689  pitonnlem2  7750