Definition df-eigval 30216

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 30323 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 29322	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 29281	. . . 4 class ℋ
4		cmap 8615	. . . 4 class ↑m
5	3, 3, 4	co 7275	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1538	. . . . 5 class 𝑡
8		cei 29321	. . . . 5 class eigvec
9	7, 8	cfv 6433	. . . 4 class (eigvec‘𝑡)
10	6	cv 1538	. . . . . . 7 class 𝑥
11	10, 7	cfv 6433	. . . . . 6 class (𝑡‘𝑥)
12		csp 29284	. . . . . 6 class ·ih
13	11, 10, 12	co 7275	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 29285	. . . . . . 7 class normℎ
15	10, 14	cfv 6433	. . . . . 6 class (normℎ‘𝑥)
16		c2 12028	. . . . . 6 class 2
17		cexp 13782	. . . . . 6 class ↑
18	15, 16, 17	co 7275	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11632	. . . . 5 class /
20	13, 18, 19	co 7275	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5157	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5157	. 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  30259