Definition df-eigval 29629

Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29736 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 28735	. 2 class eigval
2		vt	. . 3 setvar 𝑡
3		chba 28694	. . . 4 class ℋ
4		cmap 8399	. . . 4 class ↑m
5	3, 3, 4	co 7149	. . 3 class ( ℋ ↑m ℋ)
6		vx	. . . 4 setvar 𝑥
7	2	cv 1535	. . . . 5 class 𝑡
8		cei 28734	. . . . 5 class eigvec
9	7, 8	cfv 6348	. . . 4 class (eigvec‘𝑡)
10	6	cv 1535	. . . . . . 7 class 𝑥
11	10, 7	cfv 6348	. . . . . 6 class (𝑡‘𝑥)
12		csp 28697	. . . . . 6 class ·ih
13	11, 10, 12	co 7149	. . . . 5 class ((𝑡‘𝑥) ·ih 𝑥)
14		cno 28698	. . . . . . 7 class normℎ
15	10, 14	cfv 6348	. . . . . 6 class (normℎ‘𝑥)
16		c2 11686	. . . . . 6 class 2
17		cexp 13426	. . . . . 6 class ↑
18	15, 16, 17	co 7149	. . . . 5 class ((normℎ‘𝑥)↑2)
19		cdiv 11290	. . . . 5 class /
20	13, 18, 19	co 7149	. . . 4 class (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))
21	6, 9, 20	cmpt 5139	. . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))
22	2, 5, 21	cmpt 5139	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
23	1, 22	wceq 1536	1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))

This definition is referenced by:  eigvalfval  29672