Definition df-eigval 31925

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32032 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 31031	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30990	. . . 4 class ℋ
4		cmap 8773	. . . 4 class ↑m
5	3, 3, 4	co 7367	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1541	. . . . 5 class 𝑡
8		cei 31030	. . . . 5 class eigvec
9	7, 8	cfv 6498	. . . 4 class (eigvec‘𝑡)
10	6	cv 1541	. . . . . . 7 class 𝑥
11	10, 7	cfv 6498	. . . . . 6 class (𝑡‘𝑥)
12		csp 30993	. . . . . 6 class ·ih
13	11, 10, 12	co 7367	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30994	. . . . . . 7 class normℎ
15	10, 14	cfv 6498	. . . . . 6 class (normℎ‘𝑥)
16		c2 12236	. . . . . 6 class 2
17		cexp 14023	. . . . . 6 class ↑
18	15, 16, 17	co 7367	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11807	. . . . 5 class /
20	13, 18, 19	co 7367	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5166	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5166	. 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  31968