Definition df-eigval 31836

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31943 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 30942	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30901	. . . 4 class ℋ
4		cmap 8756	. . . 4 class ↑m
5	3, 3, 4	co 7352	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1540	. . . . 5 class 𝑡
8		cei 30941	. . . . 5 class eigvec
9	7, 8	cfv 6486	. . . 4 class (eigvec‘𝑡)
10	6	cv 1540	. . . . . . 7 class 𝑥
11	10, 7	cfv 6486	. . . . . 6 class (𝑡‘𝑥)
12		csp 30904	. . . . . 6 class ·ih
13	11, 10, 12	co 7352	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30905	. . . . . . 7 class normℎ
15	10, 14	cfv 6486	. . . . . 6 class (normℎ‘𝑥)
16		c2 12187	. . . . . 6 class 2
17		cexp 13970	. . . . . 6 class ↑
18	15, 16, 17	co 7352	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11781	. . . . 5 class /
20	13, 18, 19	co 7352	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5174	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5174	. 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  31879