Step |
Hyp |
Ref |
Expression |
1 |
|
pjidm.1 |
⊢ 𝐻 ∈ Cℋ |
2 |
|
pjidm.2 |
⊢ 𝐴 ∈ ℋ |
3 |
|
pjsslem.1 |
⊢ 𝐺 ∈ Cℋ |
4 |
3 2
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ |
5 |
4
|
normcli |
⊢ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ∈ ℝ |
6 |
5
|
resqcli |
⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ |
7 |
1 2
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ |
8 |
7
|
normcli |
⊢ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℝ |
9 |
8
|
resqcli |
⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ |
10 |
6 9
|
subge0i |
⊢ ( 0 ≤ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) |
11 |
|
his2sub |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) − ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) ) ) |
12 |
4 7 2 11
|
mp3an |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) − ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) ) |
13 |
3 2
|
pjinormii |
⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) |
14 |
1 2
|
pjinormii |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) |
15 |
13 14
|
oveq12i |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) − ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) |
16 |
12 15
|
eqtri |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) |
17 |
16
|
breq2i |
⊢ ( 0 ≤ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ↔ 0 ≤ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) |
18 |
|
normge0 |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) |
19 |
7 18
|
ax-mp |
⊢ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
20 |
|
normge0 |
⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
21 |
4 20
|
ax-mp |
⊢ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) |
22 |
8 5
|
le2sqi |
⊢ ( ( 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) |
23 |
19 21 22
|
mp2an |
⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) |
24 |
10 17 23
|
3bitr4i |
⊢ ( 0 ≤ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) |