Definition df-eigval 31816

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31923 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 30922	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30881	. . . 4 class ℋ
4		cmap 8760	. . . 4 class ↑m
5	3, 3, 4	co 7353	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1539	. . . . 5 class 𝑡
8		cei 30921	. . . . 5 class eigvec
9	7, 8	cfv 6486	. . . 4 class (eigvec‘𝑡)
10	6	cv 1539	. . . . . . 7 class 𝑥
11	10, 7	cfv 6486	. . . . . 6 class (𝑡‘𝑥)
12		csp 30884	. . . . . 6 class ·ih
13	11, 10, 12	co 7353	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30885	. . . . . . 7 class normℎ
15	10, 14	cfv 6486	. . . . . 6 class (normℎ‘𝑥)
16		c2 12201	. . . . . 6 class 2
17		cexp 13986	. . . . . 6 class ↑
18	15, 16, 17	co 7353	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11795	. . . . 5 class /
20	13, 18, 19	co 7353	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5176	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5176	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1540	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31859