Theorem eleigvec

Description: Membership in 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	eleigvec	|- ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eigvecval	|- ( T : ~H --> ~H -> ( eigvec ` T ) = { y e. ( ~H \ 0H ) | E. x e. CC ( T ` y ) = ( x .h y ) } )
2	1	eleq2d	|- ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> A e. { y e. ( ~H \ 0H ) | E. x e. CC ( T ` y ) = ( x .h y ) } ) )
3		eldif	|- ( A e. ( ~H \ 0H ) <-> ( A e. ~H /\ -. A e. 0H ) )
4		elch0	|- ( A e. 0H <-> A = 0h )
5	4	necon3bbii	|- ( -. A e. 0H <-> A =/= 0h )
6	5	anbi2i	|- ( ( A e. ~H /\ -. A e. 0H ) <-> ( A e. ~H /\ A =/= 0h ) )
7	3 6	bitri	|- ( A e. ( ~H \ 0H ) <-> ( A e. ~H /\ A =/= 0h ) )
8	7	anbi1i	|- ( ( A e. ( ~H \ 0H ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
9		fveq2	|- ( y = A -> ( T ` y ) = ( T ` A ) )
10		oveq2	|- ( y = A -> ( x .h y ) = ( x .h A ) )
11	9 10	eqeq12d	|- ( y = A -> ( ( T ` y ) = ( x .h y ) <-> ( T ` A ) = ( x .h A ) ) )
12	11	rexbidv	|- ( y = A -> ( E. x e. CC ( T ` y ) = ( x .h y ) <-> E. x e. CC ( T ` A ) = ( x .h A ) ) )
13	12	elrab	|- ( A e. { y e. ( ~H \ 0H ) | E. x e. CC ( T ` y ) = ( x .h y ) } <-> ( A e. ( ~H \ 0H ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
14		df-3an	|- ( ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
15	8 13 14	3bitr4i	|- ( A e. { y e. ( ~H \ 0H ) | E. x e. CC ( T ` y ) = ( x .h y ) } <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
16	2 15	bitrdi	|- ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) ) )