Definition df-eigval 31886

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31993 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 30992	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 30951	. . . 4 class ℋ
4		cmap 8884	. . . 4 class ↑m
5	3, 3, 4	co 7448	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1536	. . . . 5 class 𝑡
8		cei 30991	. . . . 5 class eigvec
9	7, 8	cfv 6573	. . . 4 class (eigvec‘𝑡)
10	6	cv 1536	. . . . . . 7 class 𝑥
11	10, 7	cfv 6573	. . . . . 6 class (𝑡‘𝑥)
12		csp 30954	. . . . . 6 class ·ih
13	11, 10, 12	co 7448	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 30955	. . . . . . 7 class normℎ
15	10, 14	cfv 6573	. . . . . 6 class (normℎ‘𝑥)
16		c2 12348	. . . . . 6 class 2
17		cexp 14112	. . . . . 6 class ↑
18	15, 16, 17	co 7448	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11947	. . . . 5 class /
20	13, 18, 19	co 7448	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5249	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5249	. 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  31929