This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjige0i

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

Ref Expression
Hypothesis pjadjt.1 
|- H e. CH
Assertion pjige0i 
|- ( A e. ~H -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) )

Proof

Step Hyp Ref Expression
1 pjadjt.1 
 |-  H e. CH
2 1 pjhcli 
 |-  ( A e. ~H -> ( ( projh ` H ) ` A ) e. ~H )
3 normcl 
 |-  ( ( ( projh ` H ) ` A ) e. ~H -> ( normh ` ( ( projh ` H ) ` A ) ) e. RR )
4 2 3 syl 
 |-  ( A e. ~H -> ( normh ` ( ( projh ` H ) ` A ) ) e. RR )
5 4 sqge0d 
 |-  ( A e. ~H -> 0 <_ ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )
6 1 pjinormi 
 |-  ( A e. ~H -> ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )
7 5 6 breqtrrd 
 |-  ( A e. ~H -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) )