Metamath Proof Explorer

Theorem addsrmo

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

Ref Expression
Assertion addsrmo ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) )

Proof

Step Hyp Ref Expression
1 enrer ⊢ ~R Er ( P × P )
2 1 a1i ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ~R Er ( P × P ) )
3 prsrlem1 ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) ∧ ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) ) )
4 addcmpblnr ⊢ ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) → ( ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) → ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ~R ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ) )
5 4 imp ⊢ ( ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) ∧ ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) ) → ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ~R ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ )
6 3 5 syl ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ~R ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ )
7 2 6 erthi ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R )
8 7 adantrlr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R )
9 8 adantrrr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) ) → [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R )
10 simprlr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) ) → 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R )
11 simprrr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) ) → 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R )
12 9 10 11 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) ) → 𝑧 = 𝑞 )
13 12 expr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → ( ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) )
14 13 exlimdvv ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → ( ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) )
15 14 exlimdvv ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) )
16 15 ex ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) ) )
17 16 exlimdvv ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) ) )
18 17 exlimdvv ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) ) )
19 18 impd ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
20 19 alrimivv ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
21 opeq12 ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ⟨ 𝑤 , 𝑣 ⟩ = ⟨ 𝑠 , 𝑓 ⟩ )
22 21 eceq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R )
23 22 eqeq2d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ↔ 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ) )
24 23 anbi1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ) )
25 simpl ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → 𝑤 = 𝑠 )
26 25 oveq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝑤 +P 𝑢 ) = ( 𝑠 +P 𝑢 ) )
27 simpr ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → 𝑣 = 𝑓 )
28 27 oveq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝑣 +P 𝑡 ) = ( 𝑓 +P 𝑡 ) )
29 26 28 opeq12d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ = ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ )
30 29 eceq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R = [ ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ ] ~R )
31 30 eqeq2d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ↔ 𝑞 = [ ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ ] ~R ) )
32 24 31 anbi12d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ ] ~R ) ) )
33 opeq12 ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ⟨ 𝑢 , 𝑡 ⟩ = ⟨ 𝑔 , ℎ ⟩ )
34 33 eceq1d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R = [ ⟨ 𝑔 , ℎ ⟩ ] ~R )
35 34 eqeq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ↔ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) )
36 35 anbi2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) )
37 simpl ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → 𝑢 = 𝑔 )
38 37 oveq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑠 +P 𝑢 ) = ( 𝑠 +P 𝑔 ) )
39 simpr ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → 𝑡 = ℎ )
40 39 oveq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑓 +P 𝑡 ) = ( 𝑓 +P ℎ ) )
41 38 40 opeq12d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ = ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ )
42 41 eceq1d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → [ ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ ] ~R = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R )
43 42 eqeq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑞 = [ ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ ] ~R ↔ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) )
44 36 43 anbi12d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑢 ) , ( 𝑓 +P 𝑡 ) ⟩ ] ~R ) ↔ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) )
45 32 44 cbvex4vw ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) )
46 45 anbi2i ⊢ ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) ↔ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) )
47 46 imbi1i ⊢ ( ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) ↔ ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
48 47 2albii ⊢ ( ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) ↔ ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑠 +P 𝑔 ) , ( 𝑓 +P ℎ ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
49 20 48 sylibr ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
50 eqeq1 ⊢ ( 𝑧 = 𝑞 → ( 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ↔ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) )
51 50 anbi2d ⊢ ( 𝑧 = 𝑞 → ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) )
52 51 4exbidv ⊢ ( 𝑧 = 𝑞 → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) )
53 52 mo4 ⊢ ( ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ↔ ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
54 49 53 sylibr ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑡 ) ⟩ ] ~R ) )