Metamath Proof Explorer


Theorem eleigvec2

Description: Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eleigvec2 T : A eigvec T A A 0 T A span A

Proof

Step Hyp Ref Expression
1 eleigvec T : A eigvec T A A 0 x T A = x A
2 elspansn A T A span A x T A = x A
3 2 adantr A A 0 T A span A x T A = x A
4 3 pm5.32i A A 0 T A span A A A 0 x T A = x A
5 df-3an A A 0 T A span A A A 0 T A span A
6 df-3an A A 0 x T A = x A A A 0 x T A = x A
7 4 5 6 3bitr4i A A 0 T A span A A A 0 x T A = x A
8 1 7 syl6bbr T : A eigvec T A A 0 T A span A