Step | Hyp | Ref
| Expression |
1 | | oveq1 7275 |
. . . . . . . . 9
⊢ ((𝐴 +P
𝐷) = (𝐵 +P 𝐶) → ((𝐴 +P 𝐷)
·P 𝐹) = ((𝐵 +P 𝐶)
·P 𝐹)) |
2 | | distrpr 10768 |
. . . . . . . . . 10
⊢ (𝐹
·P (𝐴 +P 𝐷)) = ((𝐹 ·P 𝐴) +P
(𝐹
·P 𝐷)) |
3 | | mulcompr 10763 |
. . . . . . . . . 10
⊢ ((𝐴 +P
𝐷)
·P 𝐹) = (𝐹 ·P (𝐴 +P
𝐷)) |
4 | | mulcompr 10763 |
. . . . . . . . . . 11
⊢ (𝐴
·P 𝐹) = (𝐹 ·P 𝐴) |
5 | | mulcompr 10763 |
. . . . . . . . . . 11
⊢ (𝐷
·P 𝐹) = (𝐹 ·P 𝐷) |
6 | 4, 5 | oveq12i 7280 |
. . . . . . . . . 10
⊢ ((𝐴
·P 𝐹) +P (𝐷
·P 𝐹)) = ((𝐹 ·P 𝐴) +P
(𝐹
·P 𝐷)) |
7 | 2, 3, 6 | 3eqtr4i 2777 |
. . . . . . . . 9
⊢ ((𝐴 +P
𝐷)
·P 𝐹) = ((𝐴 ·P 𝐹) +P
(𝐷
·P 𝐹)) |
8 | | distrpr 10768 |
. . . . . . . . . 10
⊢ (𝐹
·P (𝐵 +P 𝐶)) = ((𝐹 ·P 𝐵) +P
(𝐹
·P 𝐶)) |
9 | | mulcompr 10763 |
. . . . . . . . . 10
⊢ ((𝐵 +P
𝐶)
·P 𝐹) = (𝐹 ·P (𝐵 +P
𝐶)) |
10 | | mulcompr 10763 |
. . . . . . . . . . 11
⊢ (𝐵
·P 𝐹) = (𝐹 ·P 𝐵) |
11 | | mulcompr 10763 |
. . . . . . . . . . 11
⊢ (𝐶
·P 𝐹) = (𝐹 ·P 𝐶) |
12 | 10, 11 | oveq12i 7280 |
. . . . . . . . . 10
⊢ ((𝐵
·P 𝐹) +P (𝐶
·P 𝐹)) = ((𝐹 ·P 𝐵) +P
(𝐹
·P 𝐶)) |
13 | 8, 9, 12 | 3eqtr4i 2777 |
. . . . . . . . 9
⊢ ((𝐵 +P
𝐶)
·P 𝐹) = ((𝐵 ·P 𝐹) +P
(𝐶
·P 𝐹)) |
14 | 1, 7, 13 | 3eqtr3g 2802 |
. . . . . . . 8
⊢ ((𝐴 +P
𝐷) = (𝐵 +P 𝐶) → ((𝐴 ·P 𝐹) +P
(𝐷
·P 𝐹)) = ((𝐵 ·P 𝐹) +P
(𝐶
·P 𝐹))) |
15 | 14 | oveq1d 7283 |
. . . . . . 7
⊢ ((𝐴 +P
𝐷) = (𝐵 +P 𝐶) → (((𝐴 ·P 𝐹) +P
(𝐷
·P 𝐹)) +P (𝐶
·P 𝑆)) = (((𝐵 ·P 𝐹) +P
(𝐶
·P 𝐹)) +P (𝐶
·P 𝑆))) |
16 | | addasspr 10762 |
. . . . . . . 8
⊢ (((𝐵
·P 𝐹) +P (𝐶
·P 𝐹)) +P (𝐶
·P 𝑆)) = ((𝐵 ·P 𝐹) +P
((𝐶
·P 𝐹) +P (𝐶
·P 𝑆))) |
17 | | oveq2 7276 |
. . . . . . . . . 10
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → (𝐶 ·P (𝐹 +P
𝑆)) = (𝐶 ·P (𝐺 +P
𝑅))) |
18 | | distrpr 10768 |
. . . . . . . . . 10
⊢ (𝐶
·P (𝐹 +P 𝑆)) = ((𝐶 ·P 𝐹) +P
(𝐶
·P 𝑆)) |
19 | | distrpr 10768 |
. . . . . . . . . 10
⊢ (𝐶
·P (𝐺 +P 𝑅)) = ((𝐶 ·P 𝐺) +P
(𝐶
·P 𝑅)) |
20 | 17, 18, 19 | 3eqtr3g 2802 |
. . . . . . . . 9
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → ((𝐶 ·P 𝐹) +P
(𝐶
·P 𝑆)) = ((𝐶 ·P 𝐺) +P
(𝐶
·P 𝑅))) |
21 | 20 | oveq2d 7284 |
. . . . . . . 8
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → ((𝐵 ·P 𝐹) +P
((𝐶
·P 𝐹) +P (𝐶
·P 𝑆))) = ((𝐵 ·P 𝐹) +P
((𝐶
·P 𝐺) +P (𝐶
·P 𝑅)))) |
22 | 16, 21 | eqtrid 2791 |
. . . . . . 7
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → (((𝐵 ·P 𝐹) +P
(𝐶
·P 𝐹)) +P (𝐶
·P 𝑆)) = ((𝐵 ·P 𝐹) +P
((𝐶
·P 𝐺) +P (𝐶
·P 𝑅)))) |
23 | 15, 22 | sylan9eq 2799 |
. . . . . 6
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐴 ·P 𝐹) +P
(𝐷
·P 𝐹)) +P (𝐶
·P 𝑆)) = ((𝐵 ·P 𝐹) +P
((𝐶
·P 𝐺) +P (𝐶
·P 𝑅)))) |
24 | | ovex 7301 |
. . . . . . 7
⊢ (𝐴
·P 𝐹) ∈ V |
25 | | ovex 7301 |
. . . . . . 7
⊢ (𝐷
·P 𝐹) ∈ V |
26 | | ovex 7301 |
. . . . . . 7
⊢ (𝐶
·P 𝑆) ∈ V |
27 | | addcompr 10761 |
. . . . . . 7
⊢ (𝑥 +P
𝑦) = (𝑦 +P 𝑥) |
28 | | addasspr 10762 |
. . . . . . 7
⊢ ((𝑥 +P
𝑦)
+P 𝑧) = (𝑥 +P (𝑦 +P
𝑧)) |
29 | 24, 25, 26, 27, 28 | caov32 7490 |
. . . . . 6
⊢ (((𝐴
·P 𝐹) +P (𝐷
·P 𝐹)) +P (𝐶
·P 𝑆)) = (((𝐴 ·P 𝐹) +P
(𝐶
·P 𝑆)) +P (𝐷
·P 𝐹)) |
30 | | ovex 7301 |
. . . . . . 7
⊢ (𝐵
·P 𝐹) ∈ V |
31 | | ovex 7301 |
. . . . . . 7
⊢ (𝐶
·P 𝐺) ∈ V |
32 | | ovex 7301 |
. . . . . . 7
⊢ (𝐶
·P 𝑅) ∈ V |
33 | 30, 31, 32, 27, 28 | caov12 7491 |
. . . . . 6
⊢ ((𝐵
·P 𝐹) +P ((𝐶
·P 𝐺) +P (𝐶
·P 𝑅))) = ((𝐶 ·P 𝐺) +P
((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))) |
34 | 23, 29, 33 | 3eqtr3g 2802 |
. . . . 5
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐴 ·P 𝐹) +P
(𝐶
·P 𝑆)) +P (𝐷
·P 𝐹)) = ((𝐶 ·P 𝐺) +P
((𝐵
·P 𝐹) +P (𝐶
·P 𝑅)))) |
35 | 34 | oveq2d 7284 |
. . . 4
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P (((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P (𝐷
·P 𝐹))) = (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P ((𝐶
·P 𝐺) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))))) |
36 | | oveq2 7276 |
. . . . . . . . . . 11
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → (𝐷 ·P (𝐹 +P
𝑆)) = (𝐷 ·P (𝐺 +P
𝑅))) |
37 | | distrpr 10768 |
. . . . . . . . . . 11
⊢ (𝐷
·P (𝐹 +P 𝑆)) = ((𝐷 ·P 𝐹) +P
(𝐷
·P 𝑆)) |
38 | | distrpr 10768 |
. . . . . . . . . . 11
⊢ (𝐷
·P (𝐺 +P 𝑅)) = ((𝐷 ·P 𝐺) +P
(𝐷
·P 𝑅)) |
39 | 36, 37, 38 | 3eqtr3g 2802 |
. . . . . . . . . 10
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → ((𝐷 ·P 𝐹) +P
(𝐷
·P 𝑆)) = ((𝐷 ·P 𝐺) +P
(𝐷
·P 𝑅))) |
40 | 39 | oveq2d 7284 |
. . . . . . . . 9
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → ((𝐴 ·P 𝐺) +P
((𝐷
·P 𝐹) +P (𝐷
·P 𝑆))) = ((𝐴 ·P 𝐺) +P
((𝐷
·P 𝐺) +P (𝐷
·P 𝑅)))) |
41 | | addasspr 10762 |
. . . . . . . . 9
⊢ (((𝐴
·P 𝐺) +P (𝐷
·P 𝐺)) +P (𝐷
·P 𝑅)) = ((𝐴 ·P 𝐺) +P
((𝐷
·P 𝐺) +P (𝐷
·P 𝑅))) |
42 | 40, 41 | eqtr4di 2797 |
. . . . . . . 8
⊢ ((𝐹 +P
𝑆) = (𝐺 +P 𝑅) → ((𝐴 ·P 𝐺) +P
((𝐷
·P 𝐹) +P (𝐷
·P 𝑆))) = (((𝐴 ·P 𝐺) +P
(𝐷
·P 𝐺)) +P (𝐷
·P 𝑅))) |
43 | | oveq1 7275 |
. . . . . . . . . 10
⊢ ((𝐴 +P
𝐷) = (𝐵 +P 𝐶) → ((𝐴 +P 𝐷)
·P 𝐺) = ((𝐵 +P 𝐶)
·P 𝐺)) |
44 | | distrpr 10768 |
. . . . . . . . . . 11
⊢ (𝐺
·P (𝐴 +P 𝐷)) = ((𝐺 ·P 𝐴) +P
(𝐺
·P 𝐷)) |
45 | | mulcompr 10763 |
. . . . . . . . . . 11
⊢ ((𝐴 +P
𝐷)
·P 𝐺) = (𝐺 ·P (𝐴 +P
𝐷)) |
46 | | mulcompr 10763 |
. . . . . . . . . . . 12
⊢ (𝐴
·P 𝐺) = (𝐺 ·P 𝐴) |
47 | | mulcompr 10763 |
. . . . . . . . . . . 12
⊢ (𝐷
·P 𝐺) = (𝐺 ·P 𝐷) |
48 | 46, 47 | oveq12i 7280 |
. . . . . . . . . . 11
⊢ ((𝐴
·P 𝐺) +P (𝐷
·P 𝐺)) = ((𝐺 ·P 𝐴) +P
(𝐺
·P 𝐷)) |
49 | 44, 45, 48 | 3eqtr4i 2777 |
. . . . . . . . . 10
⊢ ((𝐴 +P
𝐷)
·P 𝐺) = ((𝐴 ·P 𝐺) +P
(𝐷
·P 𝐺)) |
50 | | distrpr 10768 |
. . . . . . . . . . 11
⊢ (𝐺
·P (𝐵 +P 𝐶)) = ((𝐺 ·P 𝐵) +P
(𝐺
·P 𝐶)) |
51 | | mulcompr 10763 |
. . . . . . . . . . 11
⊢ ((𝐵 +P
𝐶)
·P 𝐺) = (𝐺 ·P (𝐵 +P
𝐶)) |
52 | | mulcompr 10763 |
. . . . . . . . . . . 12
⊢ (𝐵
·P 𝐺) = (𝐺 ·P 𝐵) |
53 | | mulcompr 10763 |
. . . . . . . . . . . 12
⊢ (𝐶
·P 𝐺) = (𝐺 ·P 𝐶) |
54 | 52, 53 | oveq12i 7280 |
. . . . . . . . . . 11
⊢ ((𝐵
·P 𝐺) +P (𝐶
·P 𝐺)) = ((𝐺 ·P 𝐵) +P
(𝐺
·P 𝐶)) |
55 | 50, 51, 54 | 3eqtr4i 2777 |
. . . . . . . . . 10
⊢ ((𝐵 +P
𝐶)
·P 𝐺) = ((𝐵 ·P 𝐺) +P
(𝐶
·P 𝐺)) |
56 | 43, 49, 55 | 3eqtr3g 2802 |
. . . . . . . . 9
⊢ ((𝐴 +P
𝐷) = (𝐵 +P 𝐶) → ((𝐴 ·P 𝐺) +P
(𝐷
·P 𝐺)) = ((𝐵 ·P 𝐺) +P
(𝐶
·P 𝐺))) |
57 | 56 | oveq1d 7283 |
. . . . . . . 8
⊢ ((𝐴 +P
𝐷) = (𝐵 +P 𝐶) → (((𝐴 ·P 𝐺) +P
(𝐷
·P 𝐺)) +P (𝐷
·P 𝑅)) = (((𝐵 ·P 𝐺) +P
(𝐶
·P 𝐺)) +P (𝐷
·P 𝑅))) |
58 | 42, 57 | sylan9eqr 2801 |
. . . . . . 7
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐴 ·P 𝐺) +P
((𝐷
·P 𝐹) +P (𝐷
·P 𝑆))) = (((𝐵 ·P 𝐺) +P
(𝐶
·P 𝐺)) +P (𝐷
·P 𝑅))) |
59 | | ovex 7301 |
. . . . . . . 8
⊢ (𝐴
·P 𝐺) ∈ V |
60 | | ovex 7301 |
. . . . . . . 8
⊢ (𝐷
·P 𝑆) ∈ V |
61 | 59, 25, 60, 27, 28 | caov12 7491 |
. . . . . . 7
⊢ ((𝐴
·P 𝐺) +P ((𝐷
·P 𝐹) +P (𝐷
·P 𝑆))) = ((𝐷 ·P 𝐹) +P
((𝐴
·P 𝐺) +P (𝐷
·P 𝑆))) |
62 | | ovex 7301 |
. . . . . . . 8
⊢ (𝐵
·P 𝐺) ∈ V |
63 | | ovex 7301 |
. . . . . . . 8
⊢ (𝐷
·P 𝑅) ∈ V |
64 | 62, 31, 63, 27, 28 | caov32 7490 |
. . . . . . 7
⊢ (((𝐵
·P 𝐺) +P (𝐶
·P 𝐺)) +P (𝐷
·P 𝑅)) = (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P (𝐶
·P 𝐺)) |
65 | 58, 61, 64 | 3eqtr3g 2802 |
. . . . . 6
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P
((𝐴
·P 𝐺) +P (𝐷
·P 𝑆))) = (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P (𝐶
·P 𝐺))) |
66 | 65 | oveq1d 7283 |
. . . . 5
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐷 ·P 𝐹) +P
((𝐴
·P 𝐺) +P (𝐷
·P 𝑆))) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))) = ((((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P (𝐶
·P 𝐺)) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅)))) |
67 | | addasspr 10762 |
. . . . 5
⊢ ((((𝐵
·P 𝐺) +P (𝐷
·P 𝑅)) +P (𝐶
·P 𝐺)) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))) = (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P ((𝐶
·P 𝐺) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅)))) |
68 | 66, 67 | eqtrdi 2795 |
. . . 4
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐷 ·P 𝐹) +P
((𝐴
·P 𝐺) +P (𝐷
·P 𝑆))) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))) = (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P ((𝐶
·P 𝐺) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))))) |
69 | 35, 68 | eqtr4d 2782 |
. . 3
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐵 ·P 𝐺) +P
(𝐷
·P 𝑅)) +P (((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P (𝐷
·P 𝐹))) = (((𝐷 ·P 𝐹) +P
((𝐴
·P 𝐺) +P (𝐷
·P 𝑆))) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅)))) |
70 | | ovex 7301 |
. . . 4
⊢ ((𝐵
·P 𝐺) +P (𝐷
·P 𝑅)) ∈ V |
71 | | ovex 7301 |
. . . 4
⊢ ((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) ∈ V |
72 | 70, 71, 25, 27, 28 | caov13 7493 |
. . 3
⊢ (((𝐵
·P 𝐺) +P (𝐷
·P 𝑅)) +P (((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P (𝐷
·P 𝐹))) = ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P ((𝐵
·P 𝐺) +P (𝐷
·P 𝑅)))) |
73 | | addasspr 10762 |
. . 3
⊢ (((𝐷
·P 𝐹) +P ((𝐴
·P 𝐺) +P (𝐷
·P 𝑆))) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))) = ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐺) +P (𝐷
·P 𝑆)) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅)))) |
74 | 69, 72, 73 | 3eqtr3g 2802 |
. 2
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P ((𝐵
·P 𝐺) +P (𝐷
·P 𝑅)))) = ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐺) +P (𝐷
·P 𝑆)) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))))) |
75 | 24, 26, 62, 27, 28, 63 | caov4 7494 |
. . 3
⊢ (((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P ((𝐵
·P 𝐺) +P (𝐷
·P 𝑅))) = (((𝐴 ·P 𝐹) +P
(𝐵
·P 𝐺)) +P ((𝐶
·P 𝑆) +P (𝐷
·P 𝑅))) |
76 | 75 | oveq2i 7279 |
. 2
⊢ ((𝐷
·P 𝐹) +P (((𝐴
·P 𝐹) +P (𝐶
·P 𝑆)) +P ((𝐵
·P 𝐺) +P (𝐷
·P 𝑅)))) = ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐹) +P (𝐵
·P 𝐺)) +P ((𝐶
·P 𝑆) +P (𝐷
·P 𝑅)))) |
77 | 59, 60, 30, 27, 28, 32 | caov42 7496 |
. . 3
⊢ (((𝐴
·P 𝐺) +P (𝐷
·P 𝑆)) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅))) = (((𝐴 ·P 𝐺) +P
(𝐵
·P 𝐹)) +P ((𝐶
·P 𝑅) +P (𝐷
·P 𝑆))) |
78 | 77 | oveq2i 7279 |
. 2
⊢ ((𝐷
·P 𝐹) +P (((𝐴
·P 𝐺) +P (𝐷
·P 𝑆)) +P ((𝐵
·P 𝐹) +P (𝐶
·P 𝑅)))) = ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐺) +P (𝐵
·P 𝐹)) +P ((𝐶
·P 𝑅) +P (𝐷
·P 𝑆)))) |
79 | 74, 76, 78 | 3eqtr3g 2802 |
1
⊢ (((𝐴 +P
𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐹) +P (𝐵
·P 𝐺)) +P ((𝐶
·P 𝑆) +P (𝐷
·P 𝑅)))) = ((𝐷 ·P 𝐹) +P
(((𝐴
·P 𝐺) +P (𝐵
·P 𝐹)) +P ((𝐶
·P 𝑅) +P (𝐷
·P 𝑆))))) |