Definition df-eigval 31783

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31890 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 30889	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30848	. . . 4 class ℋ
4		cmap 8799	. . . 4 class ↑m
5	3, 3, 4	co 7387	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1539	. . . . 5 class 𝑡
8		cei 30888	. . . . 5 class eigvec
9	7, 8	cfv 6511	. . . 4 class (eigvec‘𝑡)
10	6	cv 1539	. . . . . . 7 class 𝑥
11	10, 7	cfv 6511	. . . . . 6 class (𝑡‘𝑥)
12		csp 30851	. . . . . 6 class ·ih
13	11, 10, 12	co 7387	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30852	. . . . . . 7 class normℎ
15	10, 14	cfv 6511	. . . . . 6 class (normℎ‘𝑥)
16		c2 12241	. . . . . 6 class 2
17		cexp 14026	. . . . . 6 class ↑
18	15, 16, 17	co 7387	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11835	. . . . 5 class /
20	13, 18, 19	co 7387	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5188	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5188	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1540	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31826