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