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 addridi 
 |-  ( ( ( 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 ) )