Definition df-eigval 32243

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32350 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 31349	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31308	. . . 4 class ℋ
4		cmap 8833	. . . 4 class ↑m
5	3, 3, 4	co 7423	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1569	. . . . 5 class 𝑡
8		cei 31348	. . . . 5 class eigvec
9	7, 8	cfv 6543	. . . 4 class (eigvec‘𝑡)
10	6	cv 1569	. . . . . . 7 class 𝑥
11	10, 7	cfv 6543	. . . . . 6 class (𝑡‘𝑥)
12		csp 31311	. . . . . 6 class ·ih
13	11, 10, 12	co 7423	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31312	. . . . . . 7 class normℎ
15	10, 14	cfv 6543	. . . . . 6 class (normℎ‘𝑥)
16		c2 12313	. . . . . 6 class 2
17		cexp 14117	. . . . . 6 class ↑
18	15, 16, 17	co 7423	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11889	. . . . 5 class /
20	13, 18, 19	co 7423	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5197	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5197	. 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  32286