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 ) ) ) )