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

Definition df-eigval 28097
 Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 28204 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 = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Distinct variable group:   𝑥,𝑡

Detailed syntax breakdown of Definition df-eigval
StepHypRef Expression
1 cel 27201 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chil 27160 . . . 4 class
4 cmap 7744 . . . 4 class 𝑚
53, 3, 4co 6549 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1474 . . . . 5 class 𝑡
8 cei 27200 . . . . 5 class eigvec
97, 8cfv 5804 . . . 4 class (eigvec‘𝑡)
106cv 1474 . . . . . . 7 class 𝑥
1110, 7cfv 5804 . . . . . 6 class (𝑡𝑥)
12 csp 27163 . . . . . 6 class ·ih
1311, 10, 12co 6549 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 27164 . . . . . . 7 class norm
1510, 14cfv 5804 . . . . . 6 class (norm𝑥)
16 c2 10947 . . . . . 6 class 2
17 cexp 12722 . . . . . 6 class
1815, 16, 17co 6549 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 10563 . . . . 5 class /
2013, 18, 19co 6549 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 4643 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 4643 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1475 1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
 Colors of variables: wff setvar class This definition is referenced by:  eigvalfval  28140
 Copyright terms: Public domain W3C validator