Proof of Theorem pjopyth
Step | Hyp | Ref
| Expression |
1 | | sseq1 3945 |
. . 3
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) → (𝐻 ⊆ (⊥‘𝐺) ↔ if(𝐻 ∈ Cℋ ,
𝐻, ℋ) ⊆
(⊥‘𝐺))) |
2 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
(projℎ‘𝐻) = (projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))) |
3 | 2 | fveq1d 6768 |
. . . . . . 7
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
((projℎ‘𝐻)‘𝐴) = ((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴)) |
4 | 3 | oveq1d 7282 |
. . . . . 6
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
(((projℎ‘𝐻)‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)) =
(((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴))) |
5 | 4 | fveq2d 6770 |
. . . . 5
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
(normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴))) =
(normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))) |
6 | 5 | oveq1d 7282 |
. . . 4
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2)) |
7 | 3 | fveq2d 6770 |
. . . . . 6
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
(normℎ‘((projℎ‘𝐻)‘𝐴)) =
(normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))) |
8 | 7 | oveq1d 7282 |
. . . . 5
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) =
((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2)) |
9 | 8 | oveq1d 7282 |
. . . 4
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
(((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2))) |
10 | 6, 9 | eqeq12d 2754 |
. . 3
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) →
(((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)) ↔
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)))) |
11 | 1, 10 | imbi12d 345 |
. 2
⊢ (𝐻 = if(𝐻 ∈ Cℋ ,
𝐻, ℋ) → ((𝐻 ⊆ (⊥‘𝐺) →
((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2))) ↔ (if(𝐻 ∈ Cℋ ,
𝐻, ℋ) ⊆
(⊥‘𝐺) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2))))) |
12 | | fveq2 6766 |
. . . 4
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(⊥‘𝐺) =
(⊥‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))) |
13 | 12 | sseq2d 3952 |
. . 3
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(if(𝐻 ∈
Cℋ , 𝐻, ℋ) ⊆ (⊥‘𝐺) ↔ if(𝐻 ∈ Cℋ ,
𝐻, ℋ) ⊆
(⊥‘if(𝐺 ∈
Cℋ , 𝐺, ℋ)))) |
14 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(projℎ‘𝐺) = (projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))) |
15 | 14 | fveq1d 6768 |
. . . . . . 7
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
((projℎ‘𝐺)‘𝐴) = ((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴)) |
16 | 15 | oveq2d 7283 |
. . . . . 6
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)) =
(((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴))) |
17 | 16 | fveq2d 6770 |
. . . . 5
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴))) =
(normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))) |
18 | 17 | oveq1d 7282 |
. . . 4
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))↑2)) |
19 | 15 | fveq2d 6770 |
. . . . . 6
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(normℎ‘((projℎ‘𝐺)‘𝐴)) =
(normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))) |
20 | 19 | oveq1d 7282 |
. . . . 5
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2) =
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2)) |
21 | 20 | oveq2d 7283 |
. . . 4
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2))) |
22 | 18, 21 | eqeq12d 2754 |
. . 3
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
(((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)) ↔
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2)))) |
23 | 13, 22 | imbi12d 345 |
. 2
⊢ (𝐺 = if(𝐺 ∈ Cℋ ,
𝐺, ℋ) →
((if(𝐻 ∈
Cℋ , 𝐻, ℋ) ⊆ (⊥‘𝐺) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2))) ↔ (if(𝐻 ∈ Cℋ ,
𝐻, ℋ) ⊆
(⊥‘if(𝐺 ∈
Cℋ , 𝐺, ℋ)) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2))))) |
24 | | fveq2 6766 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘𝐴) =
((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) |
25 | | fveq2 6766 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴) =
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) |
26 | 24, 25 | oveq12d 7285 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)) =
(((projℎ‘if(𝐻 ∈ Cℋ ,
𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
+ℎ ((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))) |
27 | 26 | fveq2d 6770 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴))) =
(normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
+ℎ ((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))))) |
28 | 27 | oveq1d 7282 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))↑2) =
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
+ℎ ((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))))↑2)) |
29 | 24 | fveq2d 6770 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴)) =
(normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
30 | 29 | oveq1d 7282 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) =
((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))↑2)) |
31 | 25 | fveq2d 6770 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴)) =
(normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
32 | 31 | oveq1d 7282 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2) =
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))↑2)) |
33 | 30, 32 | oveq12d 7285 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2)) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))↑2))) |
34 | 28, 33 | eqeq12d 2754 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2)) ↔
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
+ℎ ((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))↑2)))) |
35 | 34 | imbi2d 341 |
. 2
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((if(𝐻 ∈
Cℋ , 𝐻, ℋ) ⊆ (⊥‘if(𝐺 ∈
Cℋ , 𝐺, ℋ)) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴) +ℎ
((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘𝐴)))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘𝐴))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘𝐴))↑2))) ↔ (if(𝐻 ∈ Cℋ ,
𝐻, ℋ) ⊆
(⊥‘if(𝐺 ∈
Cℋ , 𝐺, ℋ)) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
+ℎ ((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))↑2))))) |
36 | | ifchhv 29614 |
. . 3
⊢ if(𝐻 ∈
Cℋ , 𝐻, ℋ) ∈
Cℋ |
37 | | ifchhv 29614 |
. . 3
⊢ if(𝐺 ∈
Cℋ , 𝐺, ℋ) ∈
Cℋ |
38 | | ifhvhv0 29392 |
. . 3
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
39 | 36, 37, 38 | pjopythi 30089 |
. 2
⊢ (if(𝐻 ∈
Cℋ , 𝐻, ℋ) ⊆ (⊥‘if(𝐺 ∈
Cℋ , 𝐺, ℋ)) →
((normℎ‘(((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
+ℎ ((projℎ‘if(𝐺 ∈ Cℋ ,
𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ))))↑2) =
(((normℎ‘((projℎ‘if(𝐻 ∈
Cℋ , 𝐻, ℋ))‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))↑2) +
((normℎ‘((projℎ‘if(𝐺 ∈
Cℋ , 𝐺, ℋ))‘if(𝐴 ∈ ℋ, 𝐴,
0ℎ)))↑2))) |
40 | 11, 23, 35, 39 | dedth3h 4519 |
1
⊢ ((𝐻 ∈
Cℋ ∧ 𝐺 ∈ Cℋ
∧ 𝐴 ∈ ℋ)
→ (𝐻 ⊆
(⊥‘𝐺) →
((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ
((projℎ‘𝐺)‘𝐴)))↑2) =
(((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) +
((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)))) |