Proof of Theorem normpyth
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵)) |
2 | 1 | eqeq1d 2624 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih 𝐵) = 0 ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0)) |
3 | | oveq1 6657 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 +ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) |
4 | 3 | fveq2d 6195 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 +ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))) |
5 | 4 | oveq1d 6665 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 +ℎ 𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2)) |
6 | | fveq2 6191 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘𝐴) = (normℎ‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) |
7 | 6 | oveq1d 6665 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘𝐴)↑2) =
((normℎ‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))↑2)) |
8 | 7 | oveq1d 6665 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘𝐴)↑2) +
((normℎ‘𝐵)↑2)) =
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘𝐵)↑2))) |
9 | 5, 8 | eqeq12d 2637 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘(𝐴 +ℎ 𝐵))↑2) =
(((normℎ‘𝐴)↑2) +
((normℎ‘𝐵)↑2)) ↔
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘𝐵)↑2)))) |
10 | 2, 9 | imbi12d 334 |
. 2
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝐴
·ih 𝐵) = 0 →
((normℎ‘(𝐴 +ℎ 𝐵))↑2) =
(((normℎ‘𝐴)↑2) +
((normℎ‘𝐵)↑2))) ↔ ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0 →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘𝐵)↑2))))) |
11 | | oveq2 6658 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
12 | 11 | eqeq1d 2624 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0 ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)) |
13 | | oveq2 6658 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ 𝐵) =
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ if(𝐵
∈ ℋ, 𝐵,
0ℎ))) |
14 | 13 | fveq2d 6195 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) |
15 | 14 | oveq1d 6665 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2)) |
16 | | fveq2 6191 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘𝐵) = (normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) |
17 | 16 | oveq1d 6665 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘𝐵)↑2) =
((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2)) |
18 | 17 | oveq2d 6666 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘𝐵)↑2)) =
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2))) |
19 | 15, 18 | eqeq12d 2637 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘𝐵)↑2)) ↔
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) = (((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)
+ ((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2)))) |
20 | 12, 19 | imbi12d 334 |
. 2
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0 →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))↑2) =
(((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2) +
((normℎ‘𝐵)↑2))) ↔ ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = 0 →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) = (((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)
+ ((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2))))) |
21 | | ifhvhv0 27879 |
. . 3
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
22 | | ifhvhv0 27879 |
. . 3
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ |
23 | 21, 22 | normpythi 27999 |
. 2
⊢
((if(𝐴 ∈
ℋ, 𝐴,
0ℎ) ·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = 0 →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))↑2) = (((normℎ‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))↑2)
+ ((normℎ‘if(𝐵 ∈ ℋ, 𝐵,
0ℎ))↑2))) |
24 | 10, 20, 23 | dedth2h 4140 |
1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴
·ih 𝐵) = 0 →
((normℎ‘(𝐴 +ℎ 𝐵))↑2) =
(((normℎ‘𝐴)↑2) +
((normℎ‘𝐵)↑2)))) |