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
|- H e. CH
pjnorm.2
|- A e. ~H
Assertion pjneli
|- ( -. A e. H <-> ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) )

Proof

Step Hyp Ref Expression
1 pjnorm.1
 |-  H e. CH
2 pjnorm.2
 |-  A e. ~H
3 1 2 pjnormi
 |-  ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` A )
4 3 biantrur
 |-  ( ( normh ` A ) =/= ( normh ` ( ( projh ` H ) ` A ) ) <-> ( ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` A ) /\ ( normh ` A ) =/= ( normh ` ( ( projh ` H ) ` A ) ) ) )
5 1 2 pjoc1i
 |-  ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
6 1 2 pjpythi
 |-  ( ( normh ` A ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) )
7 sq0
 |-  ( 0 ^ 2 ) = 0
8 7 oveq2i
 |-  ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( 0 ^ 2 ) ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + 0 )
9 1 2 pjhclii
 |-  ( ( projh ` H ) ` A ) e. ~H
10 9 normcli
 |-  ( normh ` ( ( projh ` H ) ` A ) ) e. RR
11 10 resqcli
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) e. RR
12 11 recni
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) e. CC
13 12 addid1i
 |-  ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + 0 ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 )
14 8 13 eqtr2i
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( 0 ^ 2 ) )
15 6 14 eqeq12i
 |-  ( ( ( normh ` A ) ^ 2 ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <-> ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( 0 ^ 2 ) ) )
16 1 choccli
 |-  ( _|_ ` H ) e. CH
17 16 2 pjhclii
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H
18 17 normcli
 |-  ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) e. RR
19 18 resqcli
 |-  ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) e. RR
20 19 recni
 |-  ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) e. CC
21 0cn
 |-  0 e. CC
22 21 sqcli
 |-  ( 0 ^ 2 ) e. CC
23 12 20 22 addcani
 |-  ( ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( 0 ^ 2 ) ) <-> ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) = ( 0 ^ 2 ) )
24 normge0
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H -> 0 <_ ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
25 17 24 ax-mp
 |-  0 <_ ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) )
26 0le0
 |-  0 <_ 0
27 0re
 |-  0 e. RR
28 18 27 sq11i
 |-  ( ( 0 <_ ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) /\ 0 <_ 0 ) -> ( ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) = ( 0 ^ 2 ) <-> ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 ) )
29 25 26 28 mp2an
 |-  ( ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) = ( 0 ^ 2 ) <-> ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 )
30 17 norm-i-i
 |-  ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
31 23 29 30 3bitri
 |-  ( ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( 0 ^ 2 ) ) <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
32 15 31 bitr2i
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h <-> ( ( normh ` A ) ^ 2 ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )
33 normge0
 |-  ( A e. ~H -> 0 <_ ( normh ` A ) )
34 2 33 ax-mp
 |-  0 <_ ( normh ` A )
35 normge0
 |-  ( ( ( projh ` H ) ` A ) e. ~H -> 0 <_ ( normh ` ( ( projh ` H ) ` A ) ) )
36 9 35 ax-mp
 |-  0 <_ ( normh ` ( ( projh ` H ) ` A ) )
37 2 normcli
 |-  ( normh ` A ) e. RR
38 37 10 sq11i
 |-  ( ( 0 <_ ( normh ` A ) /\ 0 <_ ( normh ` ( ( projh ` H ) ` A ) ) ) -> ( ( ( normh ` A ) ^ 2 ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <-> ( normh ` A ) = ( normh ` ( ( projh ` H ) ` A ) ) ) )
39 34 36 38 mp2an
 |-  ( ( ( normh ` A ) ^ 2 ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <-> ( normh ` A ) = ( normh ` ( ( projh ` H ) ` A ) ) )
40 5 32 39 3bitri
 |-  ( A e. H <-> ( normh ` A ) = ( normh ` ( ( projh ` H ) ` A ) ) )
41 40 necon3bbii
 |-  ( -. A e. H <-> ( normh ` A ) =/= ( normh ` ( ( projh ` H ) ` A ) ) )
42 10 37 ltleni
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) <-> ( ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` A ) /\ ( normh ` A ) =/= ( normh ` ( ( projh ` H ) ` A ) ) ) )
43 4 41 42 3bitr4i
 |-  ( -. A e. H <-> ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) )