Definition df-eigval 32115

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32222 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 31221	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31180	. . . 4 class ℋ
4		cmap 8812	. . . 4 class ↑m
5	3, 3, 4	co 7400	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1562	. . . . 5 class 𝑡
8		cei 31220	. . . . 5 class eigvec
9	7, 8	cfv 6525	. . . 4 class (eigvec‘𝑡)
10	6	cv 1562	. . . . . . 7 class 𝑥
11	10, 7	cfv 6525	. . . . . 6 class (𝑡‘𝑥)
12		csp 31183	. . . . . 6 class ·ih
13	11, 10, 12	co 7400	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31184	. . . . . . 7 class normℎ
15	10, 14	cfv 6525	. . . . . 6 class (normℎ‘𝑥)
16		c2 12286	. . . . . 6 class 2
17		cexp 14088	. . . . . 6 class ↑
18	15, 16, 17	co 7400	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11859	. . . . 5 class /
20	13, 18, 19	co 7400	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5186	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5186	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1563	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  32158