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 29053
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29160 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 28157 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chil 28116 . . . 4 class
4 cmap 8009 . . . 4 class 𝑚
53, 3, 4co 6793 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1630 . . . . 5 class 𝑡
8 cei 28156 . . . . 5 class eigvec
97, 8cfv 6031 . . . 4 class (eigvec‘𝑡)
106cv 1630 . . . . . . 7 class 𝑥
1110, 7cfv 6031 . . . . . 6 class (𝑡𝑥)
12 csp 28119 . . . . . 6 class ·ih
1311, 10, 12co 6793 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 28120 . . . . . . 7 class norm
1510, 14cfv 6031 . . . . . 6 class (norm𝑥)
16 c2 11272 . . . . . 6 class 2
17 cexp 13067 . . . . . 6 class
1815, 16, 17co 6793 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 10886 . . . . 5 class /
2013, 18, 19co 6793 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 4863 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 4863 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1631 1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  29096
  Copyright terms: Public domain W3C validator