Definition df-eigval 30970

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31077 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 30076	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30035	. . . 4 class ℋ
4		cmap 8803	. . . 4 class ↑m
5	3, 3, 4	co 7393	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1540	. . . . 5 class 𝑡
8		cei 30075	. . . . 5 class eigvec
9	7, 8	cfv 6532	. . . 4 class (eigvec‘𝑡)
10	6	cv 1540	. . . . . . 7 class 𝑥
11	10, 7	cfv 6532	. . . . . 6 class (𝑡‘𝑥)
12		csp 30038	. . . . . 6 class ·ih
13	11, 10, 12	co 7393	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30039	. . . . . . 7 class normℎ
15	10, 14	cfv 6532	. . . . . 6 class (normℎ‘𝑥)
16		c2 12249	. . . . . 6 class 2
17		cexp 14009	. . . . . 6 class ↑
18	15, 16, 17	co 7393	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11853	. . . . 5 class /
20	13, 18, 19	co 7393	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5224	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5224	. 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  31013