Metamath Proof Explorer

Theorem pjnel

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

Ref Expression
Assertion pjnel 
|- ( ( H e. CH /\ A e. ~H ) -> ( -. A e. H <-> ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( A e. H <-> A e. if ( H e. CH , H , ~H ) ) )
2 1 notbid 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( -. A e. H <-> -. A e. if ( H e. CH , H , ~H ) ) )
3 fveq2 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , ~H ) ) )
4 3 fveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( projh ` H ) ` A ) = ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) )
5 4 fveq2d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( normh ` ( ( projh ` H ) ` A ) ) = ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) )
6 5 breq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) <-> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) < ( normh ` A ) ) )
7 2 6 bibi12d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( -. A e. H <-> ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) ) <-> ( -. A e. if ( H e. CH , H , ~H ) <-> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) < ( normh ` A ) ) ) )
8 eleq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A e. if ( H e. CH , H , ~H ) <-> if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) ) )
9 8 notbid 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( -. A e. if ( H e. CH , H , ~H ) <-> -. if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) ) )
10 2fveq3 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) = ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) )
11 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` A ) = ( normh ` if ( A e. ~H , A , 0h ) ) )
12 10 11 breq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) < ( normh ` A ) <-> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) < ( normh ` if ( A e. ~H , A , 0h ) ) ) )
13 9 12 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( -. A e. if ( H e. CH , H , ~H ) <-> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) < ( normh ` A ) ) <-> ( -. if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) <-> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) < ( normh ` if ( A e. ~H , A , 0h ) ) ) ) )
14 ifchhv 
 |-  if ( H e. CH , H , ~H ) e. CH
15 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
16 14 15 pjneli 
 |-  ( -. if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) <-> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) < ( normh ` if ( A e. ~H , A , 0h ) ) )
17 7 13 16 dedth2h 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( -. A e. H <-> ( normh ` ( ( projh ` H ) ` A ) ) < ( normh ` A ) ) )