Definition df-eigval 32438

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32545 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 31544	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31503	. . . 4 class ℋ
4		cmap 8831	. . . 4 class ↑m
5	3, 3, 4	co 7412	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1569	. . . . 5 class 𝑡
8		cei 31543	. . . . 5 class eigvec
9	7, 8	cfv 6531	. . . 4 class (eigvec‘𝑡)
10	6	cv 1569	. . . . . . 7 class 𝑥
11	10, 7	cfv 6531	. . . . . 6 class (𝑡‘𝑥)
12		csp 31506	. . . . . 6 class ·ih
13	11, 10, 12	co 7412	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31507	. . . . . . 7 class normℎ
15	10, 14	cfv 6531	. . . . . 6 class (normℎ‘𝑥)
16		c2 12378	. . . . . 6 class 2
17		cexp 14184	. . . . . 6 class ↑
18	15, 16, 17	co 7412	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11954	. . . . 5 class /
20	13, 18, 19	co 7412	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5186	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5186	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1570	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is used by:  eigvalfval  32481