Definition df-eigval 32461

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32568 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 31567	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31526	. . . 4 class ℋ
4		cmap 8850	. . . 4 class ↑m
5	3, 3, 4	co 7420	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1568	. . . . 5 class 𝑡
8		cei 31566	. . . . 5 class eigvec
9	7, 8	cfv 6538	. . . 4 class (eigvec‘𝑡)
10	6	cv 1568	. . . . . . 7 class 𝑥
11	10, 7	cfv 6538	. . . . . 6 class (𝑡‘𝑥)
12		csp 31529	. . . . . 6 class ·ih
13	11, 10, 12	co 7420	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31530	. . . . . . 7 class normℎ
15	10, 14	cfv 6538	. . . . . 6 class (normℎ‘𝑥)
16		c2 12400	. . . . . 6 class 2
17		cexp 14207	. . . . . 6 class ↑
18	15, 16, 17	co 7420	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11976	. . . . 5 class /
20	13, 18, 19	co 7420	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5185	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5185	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1569	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is used by:  eigvalfval  32504