This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-eigval

Description: Define the eigenvalue function. The range of eigvalT is the set of eigenvalues of Hilbert space operator T . Theorem eigvalcl shows that ( eigvalT )A , the eigenvalue associated with eigenvector A , is a complex number. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion df-eigval 
|- eigval = ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cel 
 |-  eigval
1 vt 
 |-  t
2 chba 
 |-  ~H
3 cmap 
 |-  ^m
4 2 2 3 co 
 |-  ( ~H ^m ~H )
5 vx 
 |-  x
6 cei 
 |-  eigvec
7 1 cv 
 |-  t
8 7 6 cfv 
 |-  ( eigvec ` t )
9 5 cv 
 |-  x
10 9 7 cfv 
 |-  ( t ` x )
11 csp 
 |-  .ih
12 10 9 11 co 
 |-  ( ( t ` x ) .ih x )
13 cdiv 
 |-  /
14 cno 
 |-  normh
15 9 14 cfv 
 |-  ( normh ` x )
16 cexp 
 |-  ^
17 c2 
 |-  2
18 15 17 16 co 
 |-  ( ( normh ` x ) ^ 2 )
19 12 18 13 co 
 |-  ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) )
20 5 8 19 cmpt 
 |-  ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) )
21 1 4 20 cmpt 
 |-  ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
22 0 21 wceq 
 |-  eigval = ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )