HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-eigval Structured version   Visualization version   GIF version

Definition df-eigval 29558
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29665 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
StepHypRef Expression
1 cel 28664 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chba 28623 . . . 4 class
4 cmap 8395 . . . 4 class m
53, 3, 4co 7145 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1527 . . . . 5 class 𝑡
8 cei 28663 . . . . 5 class eigvec
97, 8cfv 6348 . . . 4 class (eigvec‘𝑡)
106cv 1527 . . . . . . 7 class 𝑥
1110, 7cfv 6348 . . . . . 6 class (𝑡𝑥)
12 csp 28626 . . . . . 6 class ·ih
1311, 10, 12co 7145 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 28627 . . . . . . 7 class norm
1510, 14cfv 6348 . . . . . 6 class (norm𝑥)
16 c2 11680 . . . . . 6 class 2
17 cexp 13417 . . . . . 6 class
1815, 16, 17co 7145 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 11285 . . . . 5 class /
2013, 18, 19co 7145 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 5137 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 5137 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1528 1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  29601
  Copyright terms: Public domain W3C validator