Theorem pjinormi

Description: The inner product of a projection and its argument is the square of the norm of the projection. Remark in Halmos p. 44. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjadjt.1	|- H e. CH
Assertion	pjinormi	|- ( A e. ~H -> ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		pjadjt.1	|- H e. CH
2		fveq2	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` H ) ` A ) = ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) )
3		id	|- ( A = if ( A e. ~H , A , 0h ) -> A = if ( A e. ~H , A , 0h ) )
4	2 3	oveq12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` H ) ` A ) .ih A ) = ( ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) .ih if ( A e. ~H , A , 0h ) ) )
5		2fveq3	|- ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( projh ` H ) ` A ) ) = ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) )
6	5	oveq1d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) = ( ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) )
7	4 6	eqeq12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <-> ( ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) .ih if ( A e. ~H , A , 0h ) ) = ( ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) ) )
8		ifhvhv0	|- if ( A e. ~H , A , 0h ) e. ~H
9	1 8	pjinormii	|- ( ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) .ih if ( A e. ~H , A , 0h ) ) = ( ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 )
10	7 9	dedth	|- ( A e. ~H -> ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )