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

Definition df-eigval 22359
Description: Define the eigenvalue function. The range of  eigval `  T is the set of eigenvalues of Hilbert space operator  T. Theorem eigvalcl 22466 shows that  ( eigval `  T
) `  A, the eigenvalue associated with eigenvector  A, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-eigval  |-  eigval  =  ( t  e.  ( ~H 
^m  ~H )  |->  ( x  e.  ( eigvec `  t
)  |->  ( ( ( t `  x ) 
.ih  x )  / 
( ( normh `  x
) ^ 2 ) ) ) )
Distinct variable group:    x, t

Detailed syntax breakdown of Definition df-eigval
StepHypRef Expression
1 cel 21465 . 2  class  eigval
2 vt . . 3  set  t
3 chil 21424 . . . 4  class  ~H
4 cmap 6705 . . . 4  class  ^m
53, 3, 4co 5757 . . 3  class  ( ~H 
^m  ~H )
6 vx . . . 4  set  x
72cv 1618 . . . . 5  class  t
8 cei 21464 . . . . 5  class  eigvec
97, 8cfv 4638 . . . 4  class  ( eigvec `  t )
106cv 1618 . . . . . . 7  class  x
1110, 7cfv 4638 . . . . . 6  class  ( t `
 x )
12 csp 21427 . . . . . 6  class  .ih
1311, 10, 12co 5757 . . . . 5  class  ( ( t `  x ) 
.ih  x )
14 cno 21428 . . . . . . 7  class  normh
1510, 14cfv 4638 . . . . . 6  class  ( normh `  x )
16 c2 9728 . . . . . 6  class  2
17 cexp 11035 . . . . . 6  class  ^
1815, 16, 17co 5757 . . . . 5  class  ( (
normh `  x ) ^
2 )
19 cdiv 9356 . . . . 5  class  /
2013, 18, 19co 5757 . . . 4  class  ( ( ( t `  x
)  .ih  x )  /  ( ( normh `  x ) ^ 2 ) )
216, 9, 20cmpt 4017 . . 3  class  ( x  e.  ( eigvec `  t
)  |->  ( ( ( t `  x ) 
.ih  x )  / 
( ( normh `  x
) ^ 2 ) ) )
222, 5, 21cmpt 4017 . 2  class  ( t  e.  ( ~H  ^m  ~H )  |->  ( x  e.  ( eigvec `  t
)  |->  ( ( ( t `  x ) 
.ih  x )  / 
( ( normh `  x
) ^ 2 ) ) ) )
231, 22wceq 1619 1  wff  eigval  =  ( t  e.  ( ~H 
^m  ~H )  |->  ( x  e.  ( eigvec `  t
)  |->  ( ( ( t `  x ) 
.ih  x )  / 
( ( normh `  x
) ^ 2 ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  eigvalfval  22402
  Copyright terms: Public domain W3C validator