Definition df-eigval 31874

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31981 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 30980	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30939	. . . 4 class ℋ
4		cmap 8867	. . . 4 class ↑m
5	3, 3, 4	co 7432	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1538	. . . . 5 class 𝑡
8		cei 30979	. . . . 5 class eigvec
9	7, 8	cfv 6560	. . . 4 class (eigvec‘𝑡)
10	6	cv 1538	. . . . . . 7 class 𝑥
11	10, 7	cfv 6560	. . . . . 6 class (𝑡‘𝑥)
12		csp 30942	. . . . . 6 class ·ih
13	11, 10, 12	co 7432	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30943	. . . . . . 7 class normℎ
15	10, 14	cfv 6560	. . . . . 6 class (normℎ‘𝑥)
16		c2 12322	. . . . . 6 class 2
17		cexp 14103	. . . . . 6 class ↑
18	15, 16, 17	co 7432	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11921	. . . . 5 class /
20	13, 18, 19	co 7432	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5224	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5224	. 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  31917