Proof of Theorem polid
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵)) |
2 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 +ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) |
3 | 2 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 +ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))) |
4 | 3 | oveq1d 6665 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 +ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2)) |
5 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 −ℎ
𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) |
6 | 5 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 −ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) |
7 | 6 | oveq1d 6665 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 −ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) |
8 | 4, 7 | oveq12d 6668 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘(𝐴 +ℎ 𝐵))↑2) −
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) =
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2))) |
9 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 +ℎ (i
·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) |
10 | 9 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵))) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))) |
11 | 10 | oveq1d 6665 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2)) |
12 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 −ℎ (i
·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))) |
13 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵))) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))) |
14 | 13 | oveq1d 6665 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)) |
15 | 11, 14 | oveq12d 6668 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) −
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2)) =
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2))) |
16 | 15 | oveq2d 6666 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (i ·
(((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) −
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2))) = (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)))) |
17 | 8, 16 | oveq12d 6668 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((((normℎ‘(𝐴 +ℎ 𝐵))↑2) −
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) −
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2)))) =
((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2))))) |
18 | 17 | oveq1d 6665 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((((normℎ‘(𝐴 +ℎ 𝐵))↑2) −
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) −
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2)))) / 4) =
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)))) /
4)) |
19 | 1, 18 | eqeq12d 2637 |
. 2
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih 𝐵) =
(((((normℎ‘(𝐴 +ℎ 𝐵))↑2) −
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) −
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2)))) / 4) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) =
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)))) /
4))) |
20 | | oveq2 6658 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
21 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ 𝐵) =
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ if(𝐵
∈ ℋ, 𝐵,
0ℎ))) |
22 | 21 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) |
23 | 22 | oveq1d 6665 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) |
24 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
25 | 24 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
26 | 25 | oveq1d 6665 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) |
27 | 23, 26 | oveq12d 6668 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) =
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2))) |
28 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (i
·ℎ 𝐵) = (i ·ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) |
29 | 28 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
30 | 29 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) |
31 | 30 | oveq1d 6665 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2)) |
32 | 28 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) |
33 | 32 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))) |
34 | 33 | oveq1d 6665 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2)) |
35 | 31, 34 | oveq12d 6668 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)) =
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2))) |
36 | 35 | oveq2d 6666 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2))) = (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2)))) |
37 | 27, 36 | oveq12d 6668 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)))) =
((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2)) + (i
· (((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2))))) |
38 | 37 | oveq1d 6665 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)))) / 4) =
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2)) + (i
· (((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2)))) / 4)) |
39 | 20, 38 | eqeq12d 2637 |
. 2
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) =
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))↑2)))) / 4) ↔
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2)) + (i
· (((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2)))) / 4))) |
40 | | ifhvhv0 27879 |
. . 3
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
41 | | ifhvhv0 27879 |
. . 3
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ |
42 | 40, 41 | polidi 28015 |
. 2
⊢ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
(((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2)) + (i
· (((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))↑2) −
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))↑2)))) / 4) |
43 | 19, 39, 42 | dedth2h 4140 |
1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴
·ih 𝐵) =
(((((normℎ‘(𝐴 +ℎ 𝐵))↑2) −
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i ·
(((normℎ‘(𝐴 +ℎ (i
·ℎ 𝐵)))↑2) −
((normℎ‘(𝐴 −ℎ (i
·ℎ 𝐵)))↑2)))) / 4)) |