Definition df-eigval 29935

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 30042 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 29041	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 29000	. . . 4 class ℋ
4		cmap 8508	. . . 4 class ↑m
5	3, 3, 4	co 7213	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1542	. . . . 5 class 𝑡
8		cei 29040	. . . . 5 class eigvec
9	7, 8	cfv 6380	. . . 4 class (eigvec‘𝑡)
10	6	cv 1542	. . . . . . 7 class 𝑥
11	10, 7	cfv 6380	. . . . . 6 class (𝑡‘𝑥)
12		csp 29003	. . . . . 6 class ·ih
13	11, 10, 12	co 7213	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 29004	. . . . . . 7 class normℎ
15	10, 14	cfv 6380	. . . . . 6 class (normℎ‘𝑥)
16		c2 11885	. . . . . 6 class 2
17		cexp 13635	. . . . . 6 class ↑
18	15, 16, 17	co 7213	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11489	. . . . 5 class /
20	13, 18, 19	co 7213	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5135	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5135	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1543	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  29978