Definition df-eigval 28713

Description: Define the eigenvalue function. The range of eigval ` T is the set of eigenvalues of Hilbert space operator T. Theorem eigvalcl 28820 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

Step	Hyp	Ref	Expression
1		cel 27817	. 2 class eigval
2		vt	. . 3 setvar t
3		chil 27776	. . . 4 class ~H
4		cmap 7857	. . . 4 class ^m
5	3, 3, 4	co 6650	. . 3 class ( ~H ^m ~H )
6		vx	. . . 4 setvar x
7	2	cv 1482	. . . . 5 class t
8		cei 27816	. . . . 5 class eigvec
9	7, 8	cfv 5888	. . . 4 class ( eigvec ` t )
10	6	cv 1482	. . . . . . 7 class x
11	10, 7	cfv 5888	. . . . . 6 class ( t ` x )
12		csp 27779	. . . . . 6 class .ih
13	11, 10, 12	co 6650	. . . . 5 class ( ( t ` x ) .ih x )
14		cno 27780	. . . . . . 7 class normh
15	10, 14	cfv 5888	. . . . . 6 class ( normh ` x )
16		c2 11070	. . . . . 6 class 2
17		cexp 12860	. . . . . 6 class ^
18	15, 16, 17	co 6650	. . . . 5 class ( ( normh ` x ) ^ 2 )
19		cdiv 10684	. . . . 5 class /
20	13, 18, 19	co 6650	. . . 4 class ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) )
21	6, 9, 20	cmpt 4729	. . 3 class ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) )
22	2, 5, 21	cmpt 4729	. 2 class ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
23	1, 22	wceq 1483	1 wff eigval = ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )

This definition is referenced by:  eigvalfval  28756