Definition df-eigval 31829

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31936 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 30935	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30894	. . . 4 class ℋ
4		cmap 8750	. . . 4 class ↑m
5	3, 3, 4	co 7346	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1540	. . . . 5 class 𝑡
8		cei 30934	. . . . 5 class eigvec
9	7, 8	cfv 6481	. . . 4 class (eigvec‘𝑡)
10	6	cv 1540	. . . . . . 7 class 𝑥
11	10, 7	cfv 6481	. . . . . 6 class (𝑡‘𝑥)
12		csp 30897	. . . . . 6 class ·ih
13	11, 10, 12	co 7346	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30898	. . . . . . 7 class normℎ
15	10, 14	cfv 6481	. . . . . 6 class (normℎ‘𝑥)
16		c2 12177	. . . . . 6 class 2
17		cexp 13965	. . . . . 6 class ↑
18	15, 16, 17	co 7346	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11771	. . . . 5 class /
20	13, 18, 19	co 7346	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5172	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5172	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1541	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31872