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 27879
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 27986 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 26983 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chil 26942 . . . 4 class
4 cmap 7624 . . . 4 class 𝑚
53, 3, 4co 6431 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1473 . . . . 5 class 𝑡
8 cei 26982 . . . . 5 class eigvec
97, 8cfv 5694 . . . 4 class (eigvec‘𝑡)
106cv 1473 . . . . . . 7 class 𝑥
1110, 7cfv 5694 . . . . . 6 class (𝑡𝑥)
12 csp 26945 . . . . . 6 class ·ih
1311, 10, 12co 6431 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 26946 . . . . . . 7 class norm
1510, 14cfv 5694 . . . . . 6 class (norm𝑥)
16 c2 10828 . . . . . 6 class 2
17 cexp 12593 . . . . . 6 class
1815, 16, 17co 6431 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 10436 . . . . 5 class /
2013, 18, 19co 6431 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 4541 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 4541 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1474 1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  27922
  Copyright terms: Public domain W3C validator