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

Definition df-eigval 22380
Description: Define the eigenvalue function. The range of  eigval `  T is the set of eigenvalues of Hilbert space operator  T. Theorem eigvalcl 22487 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 21486 . 2  class  eigval
2 vt . . 3  set  t
3 chil 21445 . . . 4  class  ~H
4 cmap 6726 . . . 4  class  ^m
53, 3, 4co 5778 . . 3  class  ( ~H 
^m  ~H )
6 vx . . . 4  set  x
72cv 1618 . . . . 5  class  t
8 cei 21485 . . . . 5  class  eigvec
97, 8cfv 4659 . . . 4  class  ( eigvec `  t )
106cv 1618 . . . . . . 7  class  x
1110, 7cfv 4659 . . . . . 6  class  ( t `
 x )
12 csp 21448 . . . . . 6  class  .ih
1311, 10, 12co 5778 . . . . 5  class  ( ( t `  x ) 
.ih  x )
14 cno 21449 . . . . . . 7  class  normh
1510, 14cfv 4659 . . . . . 6  class  ( normh `  x )
16 c2 9749 . . . . . 6  class  2
17 cexp 11056 . . . . . 6  class  ^
1815, 16, 17co 5778 . . . . 5  class  ( (
normh `  x ) ^
2 )
19 cdiv 9377 . . . . 5  class  /
2013, 18, 19co 5778 . . . 4  class  ( ( ( t `  x
)  .ih  x )  /  ( ( normh `  x ) ^ 2 ) )
216, 9, 20cmpt 4037 . . 3  class  ( x  e.  ( eigvec `  t
)  |->  ( ( ( t `  x ) 
.ih  x )  / 
( ( normh `  x
) ^ 2 ) ) )
222, 5, 21cmpt 4037 . 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  22423
  Copyright terms: Public domain W3C validator