Proof of Theorem normpar
Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7291 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 −ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) |
2 | 1 | oveq1d 7283 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 −ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2)) |
3 | | fvoveq1 7291 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 +ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))) |
4 | 3 | oveq1d 7283 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 +ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2)) |
5 | 2, 4 | oveq12d 7286 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘(𝐴 −ℎ 𝐵))↑2) +
((normℎ‘(𝐴 +ℎ 𝐵))↑2)) =
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2))) |
6 | | fveq2 6768 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘𝐴) = (normℎ‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) |
7 | 6 | oveq1d 7283 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘𝐴)↑2) =
((normℎ‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))↑2)) |
8 | 7 | oveq2d 7284 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (2 ·
((normℎ‘𝐴)↑2)) = (2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))↑2))) |
9 | 8 | oveq1d 7283 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((2 ·
((normℎ‘𝐴)↑2)) + (2 ·
((normℎ‘𝐵)↑2))) = ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘𝐵)↑2)))) |
10 | 5, 9 | eqeq12d 2755 |
. 2
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((((normℎ‘(𝐴 −ℎ 𝐵))↑2) +
((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 ·
((normℎ‘𝐴)↑2)) + (2 ·
((normℎ‘𝐵)↑2))) ↔
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2)) = ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘𝐵)↑2))))) |
11 | | oveq2 7276 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
12 | 11 | fveq2d 6772 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
13 | 12 | oveq1d 7283 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) |
14 | | oveq2 7276 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ 𝐵) =
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ if(𝐵
∈ ℋ, 𝐵,
0ℎ))) |
15 | 14 | fveq2d 6772 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) |
16 | 15 | oveq1d 7283 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) |
17 | 13, 16 | oveq12d 7286 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2)) =
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2))) |
18 | | fveq2 6768 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘𝐵) = (normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) |
19 | 18 | oveq1d 7283 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘𝐵)↑2) =
((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2)) |
20 | 19 | oveq2d 7284 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (2 ·
((normℎ‘𝐵)↑2)) = (2 ·
((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2))) |
21 | 20 | oveq2d 7284 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘𝐵)↑2))) = ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2)))) |
22 | 17, 21 | eqeq12d 2755 |
. 2
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2)) = ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘𝐵)↑2))) ↔
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) = ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2))))) |
23 | | ifhvhv0 29363 |
. . 3
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
24 | | ifhvhv0 29363 |
. . 3
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ |
25 | 23, 24 | normpari 29495 |
. 2
⊢
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))↑2) +
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) = ((2 ·
((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)) + (2
· ((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2))) |
26 | 10, 22, 25 | dedth2h 4523 |
1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
(((normℎ‘(𝐴 −ℎ 𝐵))↑2) +
((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 ·
((normℎ‘𝐴)↑2)) + (2 ·
((normℎ‘𝐵)↑2)))) |