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

Definition df-eigval 22434
 Description: Define the eigenvalue function. The range of is the set of eigenvalues of Hilbert space operator . Theorem eigvalcl 22541 shows that , the eigenvalue associated with eigenvector , is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-eigval
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-eigval
StepHypRef Expression
1 cel 21540 . 2
2 vt . . 3
3 chil 21499 . . . 4
4 cmap 6772 . . . 4
53, 3, 4co 5858 . . 3
6 vx . . . 4
72cv 1622 . . . . 5
8 cei 21539 . . . . 5
97, 8cfv 5255 . . . 4
106cv 1622 . . . . . . 7
1110, 7cfv 5255 . . . . . 6
12 csp 21502 . . . . . 6
1311, 10, 12co 5858 . . . . 5
14 cno 21503 . . . . . . 7
1510, 14cfv 5255 . . . . . 6
16 c2 9795 . . . . . 6
17 cexp 11104 . . . . . 6
1815, 16, 17co 5858 . . . . 5
19 cdiv 9423 . . . . 5
2013, 18, 19co 5858 . . . 4
216, 9, 20cmpt 4077 . . 3
222, 5, 21cmpt 4077 . 2
231, 22wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  eigvalfval  22477
 Copyright terms: Public domain W3C validator