Definition df-eigval 28713

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 28820 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 27817	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chil 27776	. . . 4 class ℋ
4		cmap 7857	. . . 4 class ↑𝑚
5	3, 3, 4	co 6650	. . 3 class ( ℋ ↑𝑚 ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1482	. . . . 5 class 𝑡
8		cei 27816	. . . . 5 class eigvec
9	7, 8	cfv 5888	. . . 4 class (eigvec‘𝑡)
10	6	cv 1482	. . . . . . 7 class 𝑥
11	10, 7	cfv 5888	. . . . . 6 class (𝑡‘𝑥)
12		csp 27779	. . . . . 6 class ·ih
13	11, 10, 12	co 6650	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 27780	. . . . . . 7 class normℎ
15	10, 14	cfv 5888	. . . . . 6 class (normℎ‘𝑥)
16		c2 11070	. . . . . 6 class 2
17		cexp 12860	. . . . . 6 class ↑
18	15, 16, 17	co 6650	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 10684	. . . . 5 class /
20	13, 18, 19	co 6650	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 4729	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 4729	. 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1483	1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  28756