Metamath Proof Explorer

Theorem mulsrpr

Description: Multiplication 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 mulsrpr ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ·R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +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 ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +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 oveq12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) = ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) )
22 17 oveq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑤 ·P 𝐷 ) = ( 𝐴 ·P 𝐷 ) )
23 19 oveq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑣 ·P 𝐶 ) = ( 𝐵 ·P 𝐶 ) )
24 22 23 oveq12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) = ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) )
25 21 24 opeq12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ = ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ )
26 25 eceq1d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R )
27 26 eqeq2d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ↔ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) )
28 16 27 anbi12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) ) )
29 28 spc2egv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ∃ 𝑤 ∃ 𝑣 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ) ) )
30 opeq12 ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ⟨ 𝑢 , 𝑡 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
31 30 eceq1d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R )
32 31 eqeq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) )
33 32 anbi2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ) )
34 simpl ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → 𝑢 = 𝐶 )
35 34 oveq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑤 ·P 𝑢 ) = ( 𝑤 ·P 𝐶 ) )
36 simpr ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → 𝑡 = 𝐷 )
37 36 oveq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑣 ·P 𝑡 ) = ( 𝑣 ·P 𝐷 ) )
38 35 37 oveq12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) = ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) )
39 36 oveq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑤 ·P 𝑡 ) = ( 𝑤 ·P 𝐷 ) )
40 34 oveq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑣 ·P 𝑢 ) = ( 𝑣 ·P 𝐶 ) )
41 39 40 oveq12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) = ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) )
42 38 41 opeq12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ = ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ )
43 42 eceq1d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R )
44 43 eqeq2d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ↔ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ) )
45 33 44 anbi12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ) ) )
46 45 spc2egv ⊢ ( ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ) → ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
47 46 2eximdv ⊢ ( ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) → ( ∃ 𝑤 ∃ 𝑣 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝐶 ) +P ( 𝑣 ·P 𝐷 ) ) , ( ( 𝑤 ·P 𝐷 ) +P ( 𝑣 ·P 𝐶 ) ) ⟩ ] ~R ) → ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
48 29 47 sylan9 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
49 11 12 48 mp2ani ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) )
50 ecexg ⊢ ( ~R ∈ V → [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ∈ V )
51 2 50 ax-mp ⊢ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ∈ V
52 simp1 ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R )
53 52 eqeq1d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ) )
54 simp2 ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R )
55 54 eqeq1d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ( 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) )
56 53 55 anbi12d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ) )
57 simp3 ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R )
58 57 eqeq1d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ( 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ↔ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) )
59 56 58 anbi12d ⊢ ( ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∧ 𝑧 = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) → ( ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~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 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
61 mulsrmo ⊢ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) → ∃* 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) )
62 df-mr ⊢ ·R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) }
63 df-nr ⊢ R = ( ( P × P ) / ~R )
64 63 eleq2i ⊢ ( 𝑥 ∈ R ↔ 𝑥 ∈ ( ( P × P ) / ~R ) )
65 63 eleq2i ⊢ ( 𝑦 ∈ R ↔ 𝑦 ∈ ( ( P × P ) / ~R ) )
66 64 65 anbi12i ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ↔ ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) )
67 66 anbi1i ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) ↔ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) )
68 67 oprabbii ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) }
69 62 68 eqtri ⊢ ·R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( ( P × P ) / ~R ) ∧ 𝑦 ∈ ( ( P × P ) / ~R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) ) }
70 60 61 69 ovig ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ∈ V ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ·R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) )
71 51 70 mp3an3 ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ) → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R = [ ⟨ ( ( 𝑤 ·P 𝑢 ) +P ( 𝑣 ·P 𝑡 ) ) , ( ( 𝑤 ·P 𝑡 ) +P ( 𝑣 ·P 𝑢 ) ) ⟩ ] ~R ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ·R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R ) )
72 8 49 71 sylc ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ·R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) = [ ⟨ ( ( 𝐴 ·P 𝐶 ) +P ( 𝐵 ·P 𝐷 ) ) , ( ( 𝐴 ·P 𝐷 ) +P ( 𝐵 ·P 𝐶 ) ) ⟩ ] ~R )