Metamath Proof Explorer

Theorem pjdifnormii

Description: Theorem 4.5(v)<->(vi) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢ 𝐻 ∈ Cℋ
pjidm.2 ⊢ 𝐴 ∈ ℋ
pjsslem.1 ⊢ 𝐺 ∈ Cℋ
Assertion pjdifnormii ( 0 ≤ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )

Proof

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ℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )