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