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 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 → A B ~ 𝑹 ⋅ 𝑹 C D ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹

Proof

Step Hyp Ref Expression
1 opelxpi ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A B ∈ 𝑷 × 𝑷
2 enrex ⊢ ~ 𝑹 ∈ V
3 2 ecelqsi ⊢ A B ∈ 𝑷 × 𝑷 → A B ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
4 1 3 syl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A B ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
5 opelxpi ⊢ C ∈ 𝑷 ∧ D ∈ 𝑷 → C D ∈ 𝑷 × 𝑷
6 2 ecelqsi ⊢ C D ∈ 𝑷 × 𝑷 → C D ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
7 5 6 syl ⊢ C ∈ 𝑷 ∧ D ∈ 𝑷 → C D ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
8 4 7 anim12i ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 → A B ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ C D ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
9 eqid ⊢ A B ~ 𝑹 = A B ~ 𝑹
10 eqid ⊢ C D ~ 𝑹 = C D ~ 𝑹
11 9 10 pm3.2i ⊢ A B ~ 𝑹 = A B ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹
12 eqid ⊢ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
13 opeq12 ⊢ w = A ∧ v = B → w v = A B
14 13 eceq1d ⊢ w = A ∧ v = B → w v ~ 𝑹 = A B ~ 𝑹
15 14 eqeq2d ⊢ w = A ∧ v = B → A B ~ 𝑹 = w v ~ 𝑹 ↔ A B ~ 𝑹 = A B ~ 𝑹
16 15 anbi1d ⊢ w = A ∧ v = B → A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ↔ A B ~ 𝑹 = A B ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹
17 simpl ⊢ w = A ∧ v = B → w = A
18 17 oveq1d ⊢ w = A ∧ v = B → w ⋅ 𝑷 C = A ⋅ 𝑷 C
19 simpr ⊢ w = A ∧ v = B → v = B
20 19 oveq1d ⊢ w = A ∧ v = B → v ⋅ 𝑷 D = B ⋅ 𝑷 D
21 18 20 oveq12d ⊢ w = A ∧ v = B → w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D
22 17 oveq1d ⊢ w = A ∧ v = B → w ⋅ 𝑷 D = A ⋅ 𝑷 D
23 19 oveq1d ⊢ w = A ∧ v = B → v ⋅ 𝑷 C = B ⋅ 𝑷 C
24 22 23 oveq12d ⊢ w = A ∧ v = B → w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C = A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C
25 21 24 opeq12d ⊢ w = A ∧ v = B → w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C
26 25 eceq1d ⊢ w = A ∧ v = B → w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
27 26 eqeq2d ⊢ w = A ∧ v = B → A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹 ↔ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
28 16 27 anbi12d ⊢ w = A ∧ v = B → A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹 ↔ A B ~ 𝑹 = A B ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
29 28 spc2egv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A B ~ 𝑹 = A B ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → ∃ w ∃ v A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹
30 opeq12 ⊢ u = C ∧ t = D → u t = C D
31 30 eceq1d ⊢ u = C ∧ t = D → u t ~ 𝑹 = C D ~ 𝑹
32 31 eqeq2d ⊢ u = C ∧ t = D → C D ~ 𝑹 = u t ~ 𝑹 ↔ C D ~ 𝑹 = C D ~ 𝑹
33 32 anbi2d ⊢ u = C ∧ t = D → A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ↔ A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹
34 simpl ⊢ u = C ∧ t = D → u = C
35 34 oveq2d ⊢ u = C ∧ t = D → w ⋅ 𝑷 u = w ⋅ 𝑷 C
36 simpr ⊢ u = C ∧ t = D → t = D
37 36 oveq2d ⊢ u = C ∧ t = D → v ⋅ 𝑷 t = v ⋅ 𝑷 D
38 35 37 oveq12d ⊢ u = C ∧ t = D → w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D
39 36 oveq2d ⊢ u = C ∧ t = D → w ⋅ 𝑷 t = w ⋅ 𝑷 D
40 34 oveq2d ⊢ u = C ∧ t = D → v ⋅ 𝑷 u = v ⋅ 𝑷 C
41 39 40 oveq12d ⊢ u = C ∧ t = D → w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u = w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C
42 38 41 opeq12d ⊢ u = C ∧ t = D → w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C
43 42 eceq1d ⊢ u = C ∧ t = D → w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹
44 43 eqeq2d ⊢ u = C ∧ t = D → A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 ↔ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹
45 33 44 anbi12d ⊢ u = C ∧ t = D → A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 ↔ A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹
46 45 spc2egv ⊢ C ∈ 𝑷 ∧ D ∈ 𝑷 → A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹 → ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
47 46 2eximdv ⊢ C ∈ 𝑷 ∧ D ∈ 𝑷 → ∃ w ∃ v A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 C + 𝑷 v ⋅ 𝑷 D w ⋅ 𝑷 D + 𝑷 v ⋅ 𝑷 C ~ 𝑹 → ∃ w ∃ v ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
48 29 47 sylan9 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 → A B ~ 𝑹 = A B ~ 𝑹 ∧ C D ~ 𝑹 = C D ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → ∃ w ∃ v ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
49 11 12 48 mp2ani ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 → ∃ w ∃ v ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
50 ecexg ⊢ ~ 𝑹 ∈ V → A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 ∈ V
51 2 50 ax-mp ⊢ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 ∈ V
52 simp1 ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → x = A B ~ 𝑹
53 52 eqeq1d ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → x = w v ~ 𝑹 ↔ A B ~ 𝑹 = w v ~ 𝑹
54 simp2 ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → y = C D ~ 𝑹
55 54 eqeq1d ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → y = u t ~ 𝑹 ↔ C D ~ 𝑹 = u t ~ 𝑹
56 53 55 anbi12d ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ↔ A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹
57 simp3 ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
58 57 eqeq1d ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 ↔ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
59 56 58 anbi12d ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 ↔ A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
60 59 4exbidv ⊢ x = A B ~ 𝑹 ∧ y = C D ~ 𝑹 ∧ z = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 → ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 ↔ ∃ w ∃ v ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
61 mulsrmo ⊢ x ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ y ∈ 𝑷 × 𝑷 / ~ 𝑹 → ∃* z ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
62 df-mr ⊢ ⋅ 𝑹 = x y z | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
63 df-nr ⊢ 𝑹 = 𝑷 × 𝑷 / ~ 𝑹
64 63 eleq2i ⊢ x ∈ 𝑹 ↔ x ∈ 𝑷 × 𝑷 / ~ 𝑹
65 63 eleq2i ⊢ y ∈ 𝑹 ↔ y ∈ 𝑷 × 𝑷 / ~ 𝑹
66 64 65 anbi12i ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ↔ x ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ y ∈ 𝑷 × 𝑷 / ~ 𝑹
67 66 anbi1i ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 ↔ x ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ y ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
68 67 oprabbii ⊢ x y z | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 = x y z | x ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ y ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
69 62 68 eqtri ⊢ ⋅ 𝑹 = x y z | x ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ y ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ t x = w v ~ 𝑹 ∧ y = u t ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹
70 60 61 69 ovig ⊢ A B ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ C D ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 ∈ V → ∃ w ∃ v ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 → A B ~ 𝑹 ⋅ 𝑹 C D ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
71 51 70 mp3an3 ⊢ A B ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 ∧ C D ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 → ∃ w ∃ v ∃ u ∃ t A B ~ 𝑹 = w v ~ 𝑹 ∧ C D ~ 𝑹 = u t ~ 𝑹 ∧ A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹 = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 t w ⋅ 𝑷 t + 𝑷 v ⋅ 𝑷 u ~ 𝑹 → A B ~ 𝑹 ⋅ 𝑹 C D ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹
72 8 49 71 sylc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 → A B ~ 𝑹 ⋅ 𝑹 C D ~ 𝑹 = A ⋅ 𝑷 C + 𝑷 B ⋅ 𝑷 D A ⋅ 𝑷 D + 𝑷 B ⋅ 𝑷 C ~ 𝑹