Metamath Proof Explorer

Theorem eigvalfval

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

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

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( eigvec ` T ) e. _V
2 1 mptex 
 |-  ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) e. _V
3 ax-hilex 
 |-  ~H e. _V
4 fveq2 
 |-  ( t = T -> ( eigvec ` t ) = ( eigvec ` T ) )
5 fveq1 
 |-  ( t = T -> ( t ` x ) = ( T ` x ) )
6 5 oveq1d 
 |-  ( t = T -> ( ( t ` x ) .ih x ) = ( ( T ` x ) .ih x ) )
7 6 oveq1d 
 |-  ( t = T -> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) = ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) )
8 4 7 mpteq12dv 
 |-  ( t = T -> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) = ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
9 df-eigval 
 |-  eigval = ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
10 2 3 3 8 9 fvmptmap 
 |-  ( T : ~H --> ~H -> ( eigval ` T ) = ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )