Definition df-eigval 31941

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32048 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 31047	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31006	. . . 4 class ℋ
4		cmap 8775	. . . 4 class ↑m
5	3, 3, 4	co 7368	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1541	. . . . 5 class 𝑡
8		cei 31046	. . . . 5 class eigvec
9	7, 8	cfv 6500	. . . 4 class (eigvec‘𝑡)
10	6	cv 1541	. . . . . . 7 class 𝑥
11	10, 7	cfv 6500	. . . . . 6 class (𝑡‘𝑥)
12		csp 31009	. . . . . 6 class ·ih
13	11, 10, 12	co 7368	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31010	. . . . . . 7 class normℎ
15	10, 14	cfv 6500	. . . . . 6 class (normℎ‘𝑥)
16		c2 12212	. . . . . 6 class 2
17		cexp 13996	. . . . . 6 class ↑
18	15, 16, 17	co 7368	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11806	. . . . 5 class /
20	13, 18, 19	co 7368	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5181	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5181	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1542	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31984