Definition df-eigval 31883

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31990 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 30989	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30948	. . . 4 class ℋ
4		cmap 8865	. . . 4 class ↑m
5	3, 3, 4	co 7431	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1536	. . . . 5 class 𝑡
8		cei 30988	. . . . 5 class eigvec
9	7, 8	cfv 6563	. . . 4 class (eigvec‘𝑡)
10	6	cv 1536	. . . . . . 7 class 𝑥
11	10, 7	cfv 6563	. . . . . 6 class (𝑡‘𝑥)
12		csp 30951	. . . . . 6 class ·ih
13	11, 10, 12	co 7431	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30952	. . . . . . 7 class normℎ
15	10, 14	cfv 6563	. . . . . 6 class (normℎ‘𝑥)
16		c2 12319	. . . . . 6 class 2
17		cexp 14099	. . . . . 6 class ↑
18	15, 16, 17	co 7431	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11918	. . . . 5 class /
20	13, 18, 19	co 7431	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5231	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5231	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1537	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  31926