Definition df-eigval 31950

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32057 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 31056	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31015	. . . 4 class ℋ
4		cmap 8770	. . . 4 class ↑m
5	3, 3, 4	co 7363	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1546	. . . . 5 class 𝑡
8		cei 31055	. . . . 5 class eigvec
9	7, 8	cfv 6492	. . . 4 class (eigvec‘𝑡)
10	6	cv 1546	. . . . . . 7 class 𝑥
11	10, 7	cfv 6492	. . . . . 6 class (𝑡‘𝑥)
12		csp 31018	. . . . . 6 class ·ih
13	11, 10, 12	co 7363	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31019	. . . . . . 7 class normℎ
15	10, 14	cfv 6492	. . . . . 6 class (normℎ‘𝑥)
16		c2 12234	. . . . . 6 class 2
17		cexp 14021	. . . . . 6 class ↑
18	15, 16, 17	co 7363	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11805	. . . . 5 class /
20	13, 18, 19	co 7363	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5160	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5160	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1547	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31993