Definition df-eigval 31374

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31481 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 30480	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30439	. . . 4 class ℋ
4		cmap 8822	. . . 4 class ↑m
5	3, 3, 4	co 7411	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1538	. . . . 5 class 𝑡
8		cei 30479	. . . . 5 class eigvec
9	7, 8	cfv 6542	. . . 4 class (eigvec‘𝑡)
10	6	cv 1538	. . . . . . 7 class 𝑥
11	10, 7	cfv 6542	. . . . . 6 class (𝑡‘𝑥)
12		csp 30442	. . . . . 6 class ·ih
13	11, 10, 12	co 7411	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30443	. . . . . . 7 class normℎ
15	10, 14	cfv 6542	. . . . . 6 class (normℎ‘𝑥)
16		c2 12271	. . . . . 6 class 2
17		cexp 14031	. . . . . 6 class ↑
18	15, 16, 17	co 7411	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11875	. . . . 5 class /
20	13, 18, 19	co 7411	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5230	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5230	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1539	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31417