Metamath Proof Explorer

Theorem eigvalval

Description: The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigvalval 
|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) = ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 eigvalfval 
 |-  ( T : ~H --> ~H -> ( eigval ` T ) = ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
2 1 fveq1d 
 |-  ( T : ~H --> ~H -> ( ( eigval ` T ) ` A ) = ( ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) ` A ) )
3 fveq2 
 |-  ( x = A -> ( T ` x ) = ( T ` A ) )
4 id 
 |-  ( x = A -> x = A )
5 3 4 oveq12d 
 |-  ( x = A -> ( ( T ` x ) .ih x ) = ( ( T ` A ) .ih A ) )
6 fveq2 
 |-  ( x = A -> ( normh ` x ) = ( normh ` A ) )
7 6 oveq1d 
 |-  ( x = A -> ( ( normh ` x ) ^ 2 ) = ( ( normh ` A ) ^ 2 ) )
8 5 7 oveq12d 
 |-  ( x = A -> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) = ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )
9 eqid 
 |-  ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) = ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) )
10 ovex 
 |-  ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) e. _V
11 8 9 10 fvmpt 
 |-  ( A e. ( eigvec ` T ) -> ( ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) ` A ) = ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )
12 2 11 sylan9eq 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) = ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )