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

Metamath Proof Explorer

Theorem pjinormii

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, 13-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
Assertion pjinormii 
|- ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
4 3 normsqi 
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) = ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` A ) )
5 1 3 2 pjadjii 
 |-  ( ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` A ) )
6 1 2 pjidmi 
 |-  ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A )
7 6 oveq1i 
 |-  ( ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( projh ` H ) ` A ) .ih A )
8 4 5 7 3eqtr2ri 
 |-  ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 )