Theorem addsrpr 6830

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 4376	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ⟨𝐴, 𝐵⟩ ∈ (P × P))
2		enrex 6822	. . . . 5 ⊢ ~R ∈ V
3	2	ecelqsi 6160	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ (P × P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
4	1, 3	syl 14	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
5		opelxpi 4376	. . . 4 ⊢ ((𝐶 ∈ P ∧ 𝐷 ∈ P) → ⟨𝐶, 𝐷⟩ ∈ (P × P))
6	2	ecelqsi 6160	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ ∈ (P × P) → [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ))
7	5, 6	syl 14	. . 3 ⊢ ((𝐶 ∈ P ∧ 𝐷 ∈ P) → [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ))
8	4, 7	anim12i 321	. 2 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R )))
9		eqid 2040	. . . 4 ⊢ [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R
10		eqid 2040	. . . 4 ⊢ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R
11	9, 10	pm3.2i 257	. . 3 ⊢ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
12		eqid 2040	. . 3 ⊢ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R
13		opeq12 3551	. . . . . . . . 9 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ⟨𝑤, 𝑣⟩ = ⟨𝐴, 𝐵⟩)
14	13	eceq1d 6142	. . . . . . . 8 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → [⟨𝑤, 𝑣⟩] ~R = [⟨𝐴, 𝐵⟩] ~R )
15	14	eqeq2d 2051	. . . . . . 7 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ))
16	15	anbi1d 438	. . . . . 6 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
17		simpl 102	. . . . . . . . . 10 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 𝑤 = 𝐴)
18	17	oveq1d 5527	. . . . . . . . 9 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑤 +P 𝐶) = (𝐴 +P 𝐶))
19		simpr 103	. . . . . . . . . 10 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
20	19	oveq1d 5527	. . . . . . . . 9 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑣 +P 𝐷) = (𝐵 +P 𝐷))
21	18, 20	opeq12d 3557	. . . . . . . 8 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩ = ⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩)
22	21	eceq1d 6142	. . . . . . 7 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
23	22	eqeq2d 2051	. . . . . 6 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ([⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
24	16, 23	anbi12d 442	. . . . 5 ⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )))
25	24	spc2egv 2642	. . . 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 3551	. . . . . . . . . 10 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ⟨𝑢, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
27	26	eceq1d 6142	. . . . . . . . 9 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → [⟨𝑢, 𝑡⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
28	27	eqeq2d 2051	. . . . . . . 8 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ([⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ))
29	28	anbi2d 437	. . . . . . 7 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
30		simpl 102	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 𝑢 = 𝐶)
31	30	oveq2d 5528	. . . . . . . . . 10 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑤 +P 𝑢) = (𝑤 +P 𝐶))
32		simpr 103	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 𝑡 = 𝐷)
33	32	oveq2d 5528	. . . . . . . . . 10 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑣 +P 𝑡) = (𝑣 +P 𝐷))
34	31, 33	opeq12d 3557	. . . . . . . . 9 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩ = ⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩)
35	34	eceq1d 6142	. . . . . . . 8 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )
36	35	eqeq2d 2051	. . . . . . 7 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ([⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ))
37	29, 36	anbi12d 442	. . . . . 6 ⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )))
38	37	spc2egv 2642	. . . . 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 1762	. . . 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 389	. . 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 408	. 2 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
42		ecexg 6110	. . . 4 ⊢ ( ~R ∈ V → [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V)
43	2, 42	ax-mp 7	. . 3 ⊢ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V
44		simp1 904	. . . . . . . 8 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑥 = [⟨𝐴, 𝐵⟩] ~R )
45	44	eqeq1d 2048	. . . . . . 7 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑥 = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ))
46		simp2 905	. . . . . . . 8 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑦 = [⟨𝐶, 𝐷⟩] ~R )
47	46	eqeq1d 2048	. . . . . . 7 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑦 = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ))
48	45, 47	anbi12d 442	. . . . . 6 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R )))
49		simp3 906	. . . . . . 7 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
50	49	eqeq1d 2048	. . . . . 6 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
51	48, 50	anbi12d 442	. . . . 5 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
52	51	4exbidv 1750	. . . 4 ⊢ ((𝑥 = [⟨𝐴, 𝐵⟩] ~R ∧ 𝑦 = [⟨𝐶, 𝐷⟩] ~R ∧ 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ ∃𝑤∃𝑣∃𝑢∃𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
53		addsrmo 6828	. . . 4 ⊢ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
54		df-plr 6813	. . . . 5 ⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
55		df-nr 6812	. . . . . . . . 9 ⊢ R = ((P × P) / ~R )
56	55	eleq2i 2104	. . . . . . . 8 ⊢ (𝑥 ∈ R ↔ 𝑥 ∈ ((P × P) / ~R ))
57	55	eleq2i 2104	. . . . . . . 8 ⊢ (𝑦 ∈ R ↔ 𝑦 ∈ ((P × P) / ~R ))
58	56, 57	anbi12i 433	. . . . . . 7 ⊢ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ↔ (𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )))
59	58	anbi1i 431	. . . . . 6 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )) ↔ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
60	59	oprabbii 5560	. . . . 5 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
61	54, 60	eqtri 2060	. . . 4 ⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
62	52, 53, 61	ovig 5622	. . 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 1221	. 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 56	1 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885   = wceq 1243  ∃wex 1381   ∈ wcel 1393  Vcvv 2557  ⟨cop 3378   × cxp 4343  (class class class)co 5512  {coprab 5513  [cec 6104   / cqs 6105  Pcnp 6389   +_P cpp 6391   ~_R cer 6394  Rcnr 6395   +_R cplr 6399

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311

This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6402  df-pli 6403  df-mi 6404  df-lti 6405  df-plpq 6442  df-mpq 6443  df-enq 6445  df-nqqs 6446  df-plqqs 6447  df-mqqs 6448  df-1nqqs 6449  df-rq 6450  df-ltnqqs 6451  df-enq0 6522  df-nq0 6523  df-0nq0 6524  df-plq0 6525  df-mq0 6526  df-inp 6564  df-iplp 6566  df-enr 6811  df-nr 6812  df-plr 6813

This theorem is referenced by:  addclsr  6838  addcomsrg  6840  addasssrg  6841  distrsrg  6844  m1p1sr  6845  0idsr  6852  ltasrg  6855  prsradd  6870  pitonnlem2  6923