Definition df-eigval 31840

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31947 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 30946	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30905	. . . 4 class ℋ
4		cmap 8845	. . . 4 class ↑m
5	3, 3, 4	co 7410	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1539	. . . . 5 class 𝑡
8		cei 30945	. . . . 5 class eigvec
9	7, 8	cfv 6536	. . . 4 class (eigvec‘𝑡)
10	6	cv 1539	. . . . . . 7 class 𝑥
11	10, 7	cfv 6536	. . . . . 6 class (𝑡‘𝑥)
12		csp 30908	. . . . . 6 class ·ih
13	11, 10, 12	co 7410	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30909	. . . . . . 7 class normℎ
15	10, 14	cfv 6536	. . . . . 6 class (normℎ‘𝑥)
16		c2 12300	. . . . . 6 class 2
17		cexp 14084	. . . . . 6 class ↑
18	15, 16, 17	co 7410	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11899	. . . . 5 class /
20	13, 18, 19	co 7410	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5206	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5206	. 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  31883