Definition df-eigval 32003

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32110 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 31109	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 31068	. . . 4 class ℋ
4		cmap 8803	. . . 4 class ↑m
5	3, 3, 4	co 7392	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1558	. . . . 5 class 𝑡
8		cei 31108	. . . . 5 class eigvec
9	7, 8	cfv 6517	. . . 4 class (eigvec‘𝑡)
10	6	cv 1558	. . . . . . 7 class 𝑥
11	10, 7	cfv 6517	. . . . . 6 class (𝑡‘𝑥)
12		csp 31071	. . . . . 6 class ·ih
13	11, 10, 12	co 7392	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 31072	. . . . . . 7 class normℎ
15	10, 14	cfv 6517	. . . . . 6 class (normℎ‘𝑥)
16		c2 12269	. . . . . 6 class 2
17		cexp 14071	. . . . . 6 class ↑
18	15, 16, 17	co 7392	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11841	. . . . 5 class /
20	13, 18, 19	co 7392	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5180	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5180	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1559	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  32046