Definition df-eigval 32184

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

Assertion

Ref	Expression
df-eigval	⊢ eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

Distinct variable group:   𝑥,𝑡

Detailed syntax breakdown of Definition df-eigval

Step	Hyp	Ref	Expression
1		cel 31290	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31249	. . . 4 class ℋ
4		cmap 8825	. . . 4 class ↑m
5	3, 3, 4	co 7412	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1569	. . . . 5 class 𝑡
8		cei 31289	. . . . 5 class eigvec
9	7, 8	cfv 6538	. . . 4 class (eigvec‘𝑡)
10	6	cv 1569	. . . . . . 7 class 𝑥
11	10, 7	cfv 6538	. . . . . 6 class (𝑡‘𝑥)
12		csp 31252	. . . . . 6 class ·ih
13	11, 10, 12	co 7412	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31253	. . . . . . 7 class normℎ
15	10, 14	cfv 6538	. . . . . 6 class (normℎ‘𝑥)
16		c2 12296	. . . . . 6 class 2
17		cexp 14099	. . . . . 6 class ↑
18	15, 16, 17	co 7412	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11872	. . . . 5 class /
20	13, 18, 19	co 7412	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5193	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5193	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1570	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  32227