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

Definition df-eigval 22264
Description: Define the eigenvalue function. The range of  eigval `  T is the set of eigenvalues of Hilbert space operator  T. Theorem eigvalcl 22371 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 21370 . 2  class  eigval
2 vt . . 3  set  t
3 chil 21329 . . . 4  class  ~H
4 cmap 6658 . . . 4  class  ^m
53, 3, 4co 5710 . . 3  class  ( ~H 
^m  ~H )
6 vx . . . 4  set  x
72cv 1618 . . . . 5  class  t
8 cei 21369 . . . . 5  class  eigvec
97, 8cfv 4592 . . . 4  class  ( eigvec `  t )
106cv 1618 . . . . . . 7  class  x
1110, 7cfv 4592 . . . . . 6  class  ( t `
 x )
12 csp 21332 . . . . . 6  class  .ih
1311, 10, 12co 5710 . . . . 5  class  ( ( t `  x ) 
.ih  x )
14 cno 21333 . . . . . . 7  class  normh
1510, 14cfv 4592 . . . . . 6  class  ( normh `  x )
16 c2 9675 . . . . . 6  class  2
17 cexp 10982 . . . . . 6  class  ^
1815, 16, 17co 5710 . . . . 5  class  ( (
normh `  x ) ^
2 )
19 cdiv 9303 . . . . 5  class  /
2013, 18, 19co 5710 . . . 4  class  ( ( ( t `  x
)  .ih  x )  /  ( ( normh `  x ) ^ 2 ) )
216, 9, 20cmpt 3974 . . 3  class  ( x  e.  ( eigvec `  t
)  |->  ( ( ( t `  x ) 
.ih  x )  / 
( ( normh `  x
) ^ 2 ) ) )
222, 5, 21cmpt 3974 . 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  22307
  Copyright terms: Public domain W3C validator