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 28841
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 28948 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 27945 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chil 27904 . . . 4 class
4 cmap 7899 . . . 4 class 𝑚
53, 3, 4co 6690 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1522 . . . . 5 class 𝑡
8 cei 27944 . . . . 5 class eigvec
97, 8cfv 5926 . . . 4 class (eigvec‘𝑡)
106cv 1522 . . . . . . 7 class 𝑥
1110, 7cfv 5926 . . . . . 6 class (𝑡𝑥)
12 csp 27907 . . . . . 6 class ·ih
1311, 10, 12co 6690 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 27908 . . . . . . 7 class norm
1510, 14cfv 5926 . . . . . 6 class (norm𝑥)
16 c2 11108 . . . . . 6 class 2
17 cexp 12900 . . . . . 6 class
1815, 16, 17co 6690 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 10722 . . . . 5 class /
2013, 18, 19co 6690 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 4762 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 4762 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1523 1 wff eigval = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  28884
  Copyright terms: Public domain W3C validator