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

Metamath Proof Explorer

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