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

Metamath Proof Explorer

Theorem eigvecval

Description: The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion eigvecval 
|- ( T : ~H --> ~H -> ( eigvec ` T ) = { x e. ( ~H \ 0H ) | E. y e. CC ( T ` x ) = ( y .h x ) } )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 difexg 
 |-  ( ~H e. _V -> ( ~H \ 0H ) e. _V )
3 1 2 ax-mp 
 |-  ( ~H \ 0H ) e. _V
4 3 rabex 
 |-  { x e. ( ~H \ 0H ) | E. y e. CC ( T ` x ) = ( y .h x ) } e. _V
5 fveq1 
 |-  ( t = T -> ( t ` x ) = ( T ` x ) )
6 5 eqeq1d 
 |-  ( t = T -> ( ( t ` x ) = ( y .h x ) <-> ( T ` x ) = ( y .h x ) ) )
7 6 rexbidv 
 |-  ( t = T -> ( E. y e. CC ( t ` x ) = ( y .h x ) <-> E. y e. CC ( T ` x ) = ( y .h x ) ) )
8 7 rabbidv 
 |-  ( t = T -> { x e. ( ~H \ 0H ) | E. y e. CC ( t ` x ) = ( y .h x ) } = { x e. ( ~H \ 0H ) | E. y e. CC ( T ` x ) = ( y .h x ) } )
9 df-eigvec 
 |-  eigvec = ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. y e. CC ( t ` x ) = ( y .h x ) } )
10 4 1 1 8 9 fvmptmap 
 |-  ( T : ~H --> ~H -> ( eigvec ` T ) = { x e. ( ~H \ 0H ) | E. y e. CC ( T ` x ) = ( y .h x ) } )