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