Definition df-eigval 28097

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 28204 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 27201	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chil 27160	. . . 4 class ℋ
4		cmap 7744	. . . 4 class ↑𝑚
5	3, 3, 4	co 6549	. . 3 class ( ℋ ↑𝑚 ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1474	. . . . 5 class 𝑡
8		cei 27200	. . . . 5 class eigvec
9	7, 8	cfv 5804	. . . 4 class (eigvec‘𝑡)
10	6	cv 1474	. . . . . . 7 class 𝑥
11	10, 7	cfv 5804	. . . . . 6 class (𝑡‘𝑥)
12		csp 27163	. . . . . 6 class ·ih
13	11, 10, 12	co 6549	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 27164	. . . . . . 7 class normℎ
15	10, 14	cfv 5804	. . . . . 6 class (normℎ‘𝑥)
16		c2 10947	. . . . . 6 class 2
17		cexp 12722	. . . . . 6 class ↑
18	15, 16, 17	co 6549	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 10563	. . . . 5 class /
20	13, 18, 19	co 6549	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 4643	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 4643	. 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1475	1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  28140