Metamath Proof Explorer

Theorem pjige0

Description: The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion pjige0 
|- ( ( H e. CH /\ A e. ~H ) -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) )
2 1 fveq1d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` H ) ` A ) = ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) )
3 2 oveq1d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( ( projh ` H ) ` A ) .ih A ) = ( ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) .ih A ) )
4 3 breq2d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) <-> 0 <_ ( ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) .ih A ) ) )
5 4 imbi2d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( A e. ~H -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) ) <-> ( A e. ~H -> 0 <_ ( ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) .ih A ) ) ) )
6 h0elch 
 |-  0H e. CH
7 6 elimel 
 |-  if ( H e. CH , H , 0H ) e. CH
8 7 pjige0i 
 |-  ( A e. ~H -> 0 <_ ( ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) .ih A ) )
9 5 8 dedth 
 |-  ( H e. CH -> ( A e. ~H -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) ) )
10 9 imp 
 |-  ( ( H e. CH /\ A e. ~H ) -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) )