Metamath Proof Explorer

Theorem mulsrmo

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

Ref Expression
Assertion mulsrmo ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +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 mulcmpblnr ⊢ ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) → ( ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) → ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ~R ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ) )
5 4 imp ⊢ ( ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) ∧ ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) ) → ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ~R ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ )
6 3 5 syl ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ~R ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ )
7 2 6 erthi ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R )
8 7 adantrlr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R )
9 8 adantrrr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) ) → [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R )
10 simprlr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) ) → 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R )
11 simprrr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) ) → 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R )
12 9 10 11 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) ) → 𝑧 = 𝑞 )
13 12 expr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → ( ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) )
14 13 exlimdvv ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → ( ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) )
15 14 exlimdvv ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) )
16 15 ex ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) ) )
17 16 exlimdvv ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) ) )
18 17 exlimdvv ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) → ( ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) → 𝑧 = 𝑞 ) ) )
19 18 impd ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
20 19 alrimivv ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +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 oveq12d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) = ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) )
30 25 oveq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝑤 ·P 𝑡 ) = ( 𝑠 ·P 𝑡 ) )
31 27 oveq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝑣 ·P 𝑢 ) = ( 𝑓 ·P 𝑢 ) )
32 30 31 oveq12d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) = ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) )
33 29 32 opeq12d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ = ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ )
34 33 eceq1d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ ] ~R )
35 34 eqeq2d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ↔ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ ] ~R ) )
36 24 35 anbi12d ⊢ ( ( 𝑤 = 𝑠 ∧ 𝑣 = 𝑓 ) → ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
37 opeq12 ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ⟨ 𝑢 , 𝑡 ⟩ = ⟨ 𝑔 , ℎ ⟩ )
38 37 eceq1d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R = [ ⟨ 𝑔 , ℎ ⟩ ] ~R )
39 38 eqeq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ↔ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) )
40 39 anbi2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) )
41 simpl ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → 𝑢 = 𝑔 )
42 41 oveq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑠 ·P 𝑢 ) = ( 𝑠 ·P 𝑔 ) )
43 simpr ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → 𝑡 = ℎ )
44 43 oveq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑓 ·P 𝑡 ) = ( 𝑓 ·P ℎ ) )
45 42 44 oveq12d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) = ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) )
46 43 oveq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑠 ·P 𝑡 ) = ( 𝑠 ·P ℎ ) )
47 41 oveq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑓 ·P 𝑢 ) = ( 𝑓 ·P 𝑔 ) )
48 46 47 oveq12d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) = ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) )
49 45 48 opeq12d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ = ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ )
50 49 eceq1d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → [ ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R )
51 50 eqeq2d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ ] ~R ↔ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) )
52 40 51 anbi12d ⊢ ( ( 𝑢 = 𝑔 ∧ 𝑡 = ℎ ) → ( ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑢 ) +P ( 𝑓 ·P 𝑡 ) ) , ( ( 𝑠 ·P 𝑡 ) +P ( 𝑓 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) )
53 36 52 cbvex4vw ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) )
54 53 anbi2i ⊢ ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) ↔ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) )
55 54 imbi1i ⊢ ( ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) ↔ ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
56 55 2albii ⊢ ( ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) ↔ ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑠 ∃ 𝑓 ∃ 𝑔 ∃ ℎ ( ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑠 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) , ( ( 𝑠 ·P ℎ ) +P ( 𝑓 ·P 𝑔 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
57 20 56 sylibr ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
58 eqeq1 ⊢ ( 𝑧 = 𝑞 → ( 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ↔ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) )
59 58 anbi2d ⊢ ( 𝑧 = 𝑞 → ( ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
60 59 4exbidv ⊢ ( 𝑧 = 𝑞 → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
61 60 mo4 ⊢ ( ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ∀ 𝑧 ∀ 𝑞 ( ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑞 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) → 𝑧 = 𝑞 ) )
62 57 61 sylibr ⊢ ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) )