Definition df-eigval 32217

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32324 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 31323	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31282	. . . 4 class ℋ
4		cmap 8822	. . . 4 class ↑m
5	3, 3, 4	co 7412	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1568	. . . . 5 class 𝑡
8		cei 31322	. . . . 5 class eigvec
9	7, 8	cfv 6536	. . . 4 class (eigvec‘𝑡)
10	6	cv 1568	. . . . . . 7 class 𝑥
11	10, 7	cfv 6536	. . . . . 6 class (𝑡‘𝑥)
12		csp 31285	. . . . . 6 class ·ih
13	11, 10, 12	co 7412	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31286	. . . . . . 7 class normℎ
15	10, 14	cfv 6536	. . . . . 6 class (normℎ‘𝑥)
16		c2 12301	. . . . . 6 class 2
17		cexp 14104	. . . . . 6 class ↑
18	15, 16, 17	co 7412	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11877	. . . . 5 class /
20	13, 18, 19	co 7412	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5191	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5191	. 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  32260