Definition df-eigval 32489

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32596 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 31595	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31554	. . . 4 class ℋ
4		cmap 8878	. . . 4 class ↑m
5	3, 3, 4	co 7446	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1569	. . . . 5 class 𝑡
8		cei 31594	. . . . 5 class eigvec
9	7, 8	cfv 6561	. . . 4 class (eigvec‘𝑡)
10	6	cv 1569	. . . . . . 7 class 𝑥
11	10, 7	cfv 6561	. . . . . 6 class (𝑡‘𝑥)
12		csp 31557	. . . . . 6 class ·ih
13	11, 10, 12	co 7446	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31558	. . . . . . 7 class normℎ
15	10, 14	cfv 6561	. . . . . 6 class (normℎ‘𝑥)
16		c2 12427	. . . . . 6 class 2
17		cexp 14234	. . . . . 6 class ↑
18	15, 16, 17	co 7446	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 12003	. . . . 5 class /
20	13, 18, 19	co 7446	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5190	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5190	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1570	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is used by:  eigvalfval  32532