Definition df-eigval 29285

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29392 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 = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

Distinct variable group:   𝑥,𝑡

Detailed syntax breakdown of Definition df-eigval

Step	Hyp	Ref	Expression
1		cel 28389	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 28348	. . . 4 class ℋ
4		cmap 8140	. . . 4 class ↑𝑚
5	3, 3, 4	co 6922	. . 3 class ( ℋ ↑𝑚 ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1600	. . . . 5 class 𝑡
8		cei 28388	. . . . 5 class eigvec
9	7, 8	cfv 6135	. . . 4 class (eigvec‘𝑡)
10	6	cv 1600	. . . . . . 7 class 𝑥
11	10, 7	cfv 6135	. . . . . 6 class (𝑡‘𝑥)
12		csp 28351	. . . . . 6 class ·ih
13	11, 10, 12	co 6922	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 28352	. . . . . . 7 class normℎ
15	10, 14	cfv 6135	. . . . . 6 class (normℎ‘𝑥)
16		c2 11430	. . . . . 6 class 2
17		cexp 13178	. . . . . 6 class ↑
18	15, 16, 17	co 6922	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11032	. . . . 5 class /
20	13, 18, 19	co 6922	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 4965	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 4965	. 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1601	1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  29328