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

Definition df-eigvec 23356
 Description: Define the eigenvector function. Theorem eleigveccl 23462 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 22462 . 2
2 vt . . 3
3 chil 22422 . . . 4
4 cmap 7018 . . . 4
53, 3, 4co 6081 . . 3
6 vx . . . . . . . 8
76cv 1651 . . . . . . 7
82cv 1651 . . . . . . 7
97, 8cfv 5454 . . . . . 6
10 vz . . . . . . . 8
1110cv 1651 . . . . . . 7
12 csm 22424 . . . . . . 7
1311, 7, 12co 6081 . . . . . 6
149, 13wceq 1652 . . . . 5
15 cc 8988 . . . . 5
1614, 10, 15wrex 2706 . . . 4
17 c0h 22438 . . . . 5
183, 17cdif 3317 . . . 4
1916, 6, 18crab 2709 . . 3
202, 5, 19cmpt 4266 . 2
211, 20wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  eigvecval  23399
 Copyright terms: Public domain W3C validator