Definition df-eigval 31940

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32047 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 31046	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31005	. . . 4 class ℋ
4		cmap 8766	. . . 4 class ↑m
5	3, 3, 4	co 7360	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1541	. . . . 5 class 𝑡
8		cei 31045	. . . . 5 class eigvec
9	7, 8	cfv 6492	. . . 4 class (eigvec‘𝑡)
10	6	cv 1541	. . . . . . 7 class 𝑥
11	10, 7	cfv 6492	. . . . . 6 class (𝑡‘𝑥)
12		csp 31008	. . . . . 6 class ·ih
13	11, 10, 12	co 7360	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31009	. . . . . . 7 class normℎ
15	10, 14	cfv 6492	. . . . . 6 class (normℎ‘𝑥)
16		c2 12227	. . . . . 6 class 2
17		cexp 14014	. . . . . 6 class ↑
18	15, 16, 17	co 7360	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11798	. . . . 5 class /
20	13, 18, 19	co 7360	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5167	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5167	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1542	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31983