Definition df-eigval 31790

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31897 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 30896	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30855	. . . 4 class ℋ
4		cmap 8802	. . . 4 class ↑m
5	3, 3, 4	co 7390	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1539	. . . . 5 class 𝑡
8		cei 30895	. . . . 5 class eigvec
9	7, 8	cfv 6514	. . . 4 class (eigvec‘𝑡)
10	6	cv 1539	. . . . . . 7 class 𝑥
11	10, 7	cfv 6514	. . . . . 6 class (𝑡‘𝑥)
12		csp 30858	. . . . . 6 class ·ih
13	11, 10, 12	co 7390	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30859	. . . . . . 7 class normℎ
15	10, 14	cfv 6514	. . . . . 6 class (normℎ‘𝑥)
16		c2 12248	. . . . . 6 class 2
17		cexp 14033	. . . . . 6 class ↑
18	15, 16, 17	co 7390	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11842	. . . . 5 class /
20	13, 18, 19	co 7390	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5191	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5191	. 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  31833