Step |
Hyp |
Ref |
Expression |
1 |
|
pjidm.1 |
⊢ 𝐻 ∈ Cℋ |
2 |
|
pjidm.2 |
⊢ 𝐴 ∈ ℋ |
3 |
|
pjsslem.1 |
⊢ 𝐺 ∈ Cℋ |
4 |
1
|
choccli |
⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ |
5 |
3 4
|
chincli |
⊢ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ∈ Cℋ |
6 |
5 2
|
pjhclii |
⊢ ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ∈ ℋ |
7 |
6
|
normcli |
⊢ ( normℎ ‘ ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ∈ ℝ |
8 |
7
|
sqge0i |
⊢ 0 ≤ ( ( normℎ ‘ ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↑ 2 ) |
9 |
|
oveq1 |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ·ih 𝐴 ) ) |
10 |
5 2
|
pjinormii |
⊢ ( ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↑ 2 ) |
11 |
9 10
|
eqtrdi |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↑ 2 ) ) |
12 |
8 11
|
breqtrrid |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → 0 ≤ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ) |