Metamath Proof Explorer

Theorem 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 ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R +R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R )

Proof

Step Hyp Ref Expression
1 opelxpi ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( P × P ) )
2 enrex ⊢ ~R ∈ V
3 2 ecelqsi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( P × P ) → [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
4 1 3 syl ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
5 opelxpi ⊢ ( ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( P × P ) )
6 2 ecelqsi ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( P × P ) → [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
7 5 6 syl ⊢ ( ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) → [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
8 4 7 anim12i ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ) )
9 eqid ⊢ [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R
10 eqid ⊢ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R
11 9 10 pm3.2i ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R )
12 eqid ⊢ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R
13 opeq12 ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ⟨ 𝑤 , 𝑣 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
14 13 eceq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R )
15 14 eqeq2d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ) )
16 15 anbi1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ) )
17 simpl ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → 𝑤 = 𝐴 )
18 17 oveq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑤 +P 𝐶 ) = ( 𝐴 +P 𝐶 ) )
19 simpr ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → 𝑣 = 𝐵 )
20 19 oveq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑣 +P 𝐷 ) = ( 𝐵 +P 𝐷 ) )
21 18 20 opeq12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ = ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ )
22 21 eceq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R )
23 22 eqeq2d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R ↔ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) )
24 16 23 anbi12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) ) )
25 24 spc2egv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ∃ 𝑤 ∃ 𝑣 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R ) ) )
26 opeq12 ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ⟨ 𝑢 , 𝑡 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
27 26 eceq1d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R )
28 27 eqeq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) )
29 28 anbi2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ) )
30 simpl ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → 𝑢 = 𝐶 )
31 30 oveq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑤 +P 𝑢 ) = ( 𝑤 +P 𝐶 ) )
32 simpr ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → 𝑡 = 𝐷 )
33 32 oveq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑣 +P 𝑡 ) = ( 𝑣 +P 𝐷 ) )
34 31 33 opeq12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ = ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ )
35 34 eceq1d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R )
36 35 eqeq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ↔ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R ) )
37 29 36 anbi12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝐶 ) , ( 𝑣 +P 𝐷 ) ⟩ ] ~R ) ) )
38 37 spc2egv ⊢ ( ( 𝐶 ∈ 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 ⊢ ( ( 𝐶 ∈ 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 ⊢ ( ( ( 𝐴 ∈ 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 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) )
42 ecexg ⊢ ( ~R ∈ V → [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ∈ V )
43 2 42 ax-mp ⊢ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ∈ V
44 simp1 ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R )
45 44 eqeq1d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ) )
46 simp2 ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R )
47 46 eqeq1d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ( 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) )
48 45 47 anbi12d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ) )
49 simp3 ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R )
50 49 eqeq1d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ( 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ↔ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) )
51 48 50 anbi12d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ( ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) )
52 51 4exbidv ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) )
53 addsrmo ⊢ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) )
54 df-plr ⊢ +R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) }
55 df-nr ⊢ R = ( ( P × P ) / ~R )
56 55 eleq2i ⊢ ( 𝑥 ∈ R ↔ 𝑥 ∈ ( ( P × P ) / ~R ) )
57 55 eleq2i ⊢ ( 𝑦 ∈ R ↔ 𝑦 ∈ ( ( P × P ) / ~R ) )
58 56 57 anbi12i ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ↔ ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) )
59 58 anbi1i ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) ↔ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) )
60 59 oprabbii ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) }
61 54 60 eqtri ⊢ +R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) }
62 52 53 61 ovig ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~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 ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~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 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R +R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) = [ ⟨ ( 𝐴 +P 𝐶 ) , ( 𝐵 +P 𝐷 ) ⟩ ] ~R )