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 : A eigvec T A A 0 x T A = x A

Proof

Step Hyp Ref Expression
1 eigvecval T : eigvec T = y 0 | x T y = x y
2 1 eleq2d T : A eigvec T A y 0 | x T y = x y
3 eldif A 0 A ¬ A 0
4 elch0 A 0 A = 0
5 4 necon3bbii ¬ A 0 A 0
6 5 anbi2i A ¬ A 0 A A 0
7 3 6 bitri A 0 A A 0
8 7 anbi1i A 0 x T A = x A A A 0 x T A = x A
9 fveq2 y = A T y = T A
10 oveq2 y = A x y = x A
11 9 10 eqeq12d y = A T y = x y T A = x A
12 11 rexbidv y = A x T y = x y x T A = x A
13 12 elrab A y 0 | x T y = x y A 0 x T A = x A
14 df-3an A A 0 x T A = x A A A 0 x T A = x A
15 8 13 14 3bitr4i A y 0 | x T y = x y A A 0 x T A = x A
16 2 15 bitrdi T : A eigvec T A A 0 x T A = x A