Metamath Proof Explorer

Theorem pjneli

Description: If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjnorm.1 ⊢ 𝐻 ∈ Cℋ
pjnorm.2 ⊢ 𝐴 ∈ ℋ
Assertion pjneli ( ¬ 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjnorm.1 ⊢ 𝐻 ∈ Cℋ
2 pjnorm.2 ⊢ 𝐴 ∈ ℋ
3 1 2 pjnormi ⊢ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 )
4 3 biantrur ⊢ ( ( normℎ ‘ 𝐴 ) ≠ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) ∧ ( normℎ ‘ 𝐴 ) ≠ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) )
5 1 2 pjoc1i ⊢ ( 𝐴 ∈ 𝐻 ↔ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ )
6 1 2 pjpythi ⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) )
7 sq0 ⊢ ( 0 ↑ 2 ) = 0
8 7 oveq2i ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( 0 ↑ 2 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + 0 )
9 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
10 9 normcli ⊢ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℝ
11 10 resqcli ⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ
12 11 recni ⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℂ
13 12 addridi ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + 0 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 )
14 8 13 eqtr2i ⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( 0 ↑ 2 ) )
15 6 14 eqeq12i ⊢ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ↔ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( 0 ↑ 2 ) ) )
16 1 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
17 16 2 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ
18 17 normcli ⊢ ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ∈ ℝ
19 18 resqcli ⊢ ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ
20 19 recni ⊢ ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℂ
21 0cn ⊢ 0 ∈ ℂ
22 21 sqcli ⊢ ( 0 ↑ 2 ) ∈ ℂ
23 12 20 22 addcani ⊢ ( ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( 0 ↑ 2 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) = ( 0 ↑ 2 ) )
24 normge0 ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
25 17 24 ax-mp ⊢ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )
26 0le0 ⊢ 0 ≤ 0
27 0re ⊢ 0 ∈ ℝ
28 18 27 sq11i ⊢ ( ( 0 ≤ ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ∧ 0 ≤ 0 ) → ( ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) = ( 0 ↑ 2 ) ↔ ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = 0 ) )
29 25 26 28 mp2an ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) = ( 0 ↑ 2 ) ↔ ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = 0 )
30 17 norm-i-i ⊢ ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = 0 ↔ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ )
31 23 29 30 3bitri ⊢ ( ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( 0 ↑ 2 ) ) ↔ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ )
32 15 31 bitr2i ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ ↔ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) )
33 normge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
34 2 33 ax-mp ⊢ 0 ≤ ( normℎ ‘ 𝐴 )
35 normge0 ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
36 9 35 ax-mp ⊢ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )
37 2 normcli ⊢ ( normℎ ‘ 𝐴 ) ∈ ℝ
38 37 10 sq11i ⊢ ( ( 0 ≤ ( normℎ ‘ 𝐴 ) ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) → ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ↔ ( normℎ ‘ 𝐴 ) = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) )
39 34 36 38 mp2an ⊢ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ↔ ( normℎ ‘ 𝐴 ) = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
40 5 32 39 3bitri ⊢ ( 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ 𝐴 ) = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
41 40 necon3bbii ⊢ ( ¬ 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ 𝐴 ) ≠ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
42 10 37 ltleni ⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) ∧ ( normℎ ‘ 𝐴 ) ≠ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) )
43 4 41 42 3bitr4i ⊢ ( ¬ 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) )