Definition df-eigval 32343

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32450 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 31449	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31408	. . . 4 class ℋ
4		cmap 8830	. . . 4 class ↑m
5	3, 3, 4	co 7417	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1569	. . . . 5 class 𝑡
8		cei 31448	. . . . 5 class eigvec
9	7, 8	cfv 6537	. . . 4 class (eigvec‘𝑡)
10	6	cv 1569	. . . . . . 7 class 𝑥
11	10, 7	cfv 6537	. . . . . 6 class (𝑡‘𝑥)
12		csp 31411	. . . . . 6 class ·ih
13	11, 10, 12	co 7417	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31412	. . . . . . 7 class normℎ
15	10, 14	cfv 6537	. . . . . 6 class (normℎ‘𝑥)
16		c2 12323	. . . . . 6 class 2
17		cexp 14129	. . . . . 6 class ↑
18	15, 16, 17	co 7417	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11899	. . . . 5 class /
20	13, 18, 19	co 7417	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5190	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5190	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1570	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is used by:  eigvalfval  32386