Definition df-eigval 31102

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31209 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 30208	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30167	. . . 4 class ℋ
4		cmap 8819	. . . 4 class ↑m
5	3, 3, 4	co 7408	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1540	. . . . 5 class 𝑡
8		cei 30207	. . . . 5 class eigvec
9	7, 8	cfv 6543	. . . 4 class (eigvec‘𝑡)
10	6	cv 1540	. . . . . . 7 class 𝑥
11	10, 7	cfv 6543	. . . . . 6 class (𝑡‘𝑥)
12		csp 30170	. . . . . 6 class ·ih
13	11, 10, 12	co 7408	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30171	. . . . . . 7 class normℎ
15	10, 14	cfv 6543	. . . . . 6 class (normℎ‘𝑥)
16		c2 12266	. . . . . 6 class 2
17		cexp 14026	. . . . . 6 class ↑
18	15, 16, 17	co 7408	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11870	. . . . 5 class /
20	13, 18, 19	co 7408	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5231	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5231	. 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  31145