Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-eigvec Unicode version

Definition df-eigvec 22263
 Description: Define the eigenvector function. Theorem eleigveccl 22369 shows that , the set of eigenvectors of Hilbert space operator , are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-eigvec
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-eigvec
StepHypRef Expression
1 cei 21369 . 2
2 vt . . 3
3 chil 21329 . . . 4
4 cmap 6658 . . . 4
53, 3, 4co 5710 . . 3
6 vx . . . . . . . 8
76cv 1618 . . . . . . 7
82cv 1618 . . . . . . 7
97, 8cfv 4592 . . . . . 6
10 vz . . . . . . . 8
1110cv 1618 . . . . . . 7
12 csm 21331 . . . . . . 7
1311, 7, 12co 5710 . . . . . 6
149, 13wceq 1619 . . . . 5
15 cc 8615 . . . . 5
1614, 10, 15wrex 2510 . . . 4
17 c0h 21345 . . . . 5
183, 17cdif 3075 . . . 4
1916, 6, 18crab 2512 . . 3
202, 5, 19cmpt 3974 . 2
211, 20wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  eigvecval  22306
 Copyright terms: Public domain W3C validator