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

Metamath Proof Explorer

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