Metamath Proof Explorer


Definition df-eigvec

Description: Define the eigenvector function. Theorem eleigveccl shows that eigvecT , the set of eigenvectors of Hilbert space operator T , are Hilbert space vectors. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion df-eigvec eigvec = t x 0 | z t x = z x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cei class eigvec
1 vt setvar t
2 chba class
3 cmap class 𝑚
4 2 2 3 co class
5 vx setvar x
6 c0h class 0
7 2 6 cdif class 0
8 vz setvar z
9 cc class
10 1 cv setvar t
11 5 cv setvar x
12 11 10 cfv class t x
13 8 cv setvar z
14 csm class
15 13 11 14 co class z x
16 12 15 wceq wff t x = z x
17 16 8 9 wrex wff z t x = z x
18 17 5 7 crab class x 0 | z t x = z x
19 1 4 18 cmpt class t x 0 | z t x = z x
20 0 19 wceq wff eigvec = t x 0 | z t x = z x