Definition df-eigval 31929

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32036 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 31035	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30994	. . . 4 class ℋ
4		cmap 8763	. . . 4 class ↑m
5	3, 3, 4	co 7358	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1540	. . . . 5 class 𝑡
8		cei 31034	. . . . 5 class eigvec
9	7, 8	cfv 6492	. . . 4 class (eigvec‘𝑡)
10	6	cv 1540	. . . . . . 7 class 𝑥
11	10, 7	cfv 6492	. . . . . 6 class (𝑡‘𝑥)
12		csp 30997	. . . . . 6 class ·ih
13	11, 10, 12	co 7358	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30998	. . . . . . 7 class normℎ
15	10, 14	cfv 6492	. . . . . 6 class (normℎ‘𝑥)
16		c2 12200	. . . . . 6 class 2
17		cexp 13984	. . . . . 6 class ↑
18	15, 16, 17	co 7358	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11794	. . . . 5 class /
20	13, 18, 19	co 7358	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5179	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5179	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1541	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31972