Definition df-eigval 30117

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 30224 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 29223	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 29182	. . . 4 class ℋ
4		cmap 8573	. . . 4 class ↑m
5	3, 3, 4	co 7255	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1538	. . . . 5 class 𝑡
8		cei 29222	. . . . 5 class eigvec
9	7, 8	cfv 6418	. . . 4 class (eigvec‘𝑡)
10	6	cv 1538	. . . . . . 7 class 𝑥
11	10, 7	cfv 6418	. . . . . 6 class (𝑡‘𝑥)
12		csp 29185	. . . . . 6 class ·ih
13	11, 10, 12	co 7255	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 29186	. . . . . . 7 class normℎ
15	10, 14	cfv 6418	. . . . . 6 class (normℎ‘𝑥)
16		c2 11958	. . . . . 6 class 2
17		cexp 13710	. . . . . 6 class ↑
18	15, 16, 17	co 7255	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11562	. . . . 5 class /
20	13, 18, 19	co 7255	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5153	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5153	. 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  30160