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

Definition df-eigval 29678
 Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29785 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 28784 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chba 28743 . . . 4 class
4 cmap 8404 . . . 4 class m
53, 3, 4co 7142 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1537 . . . . 5 class 𝑡
8 cei 28783 . . . . 5 class eigvec
97, 8cfv 6329 . . . 4 class (eigvec‘𝑡)
106cv 1537 . . . . . . 7 class 𝑥
1110, 7cfv 6329 . . . . . 6 class (𝑡𝑥)
12 csp 28746 . . . . . 6 class ·ih
1311, 10, 12co 7142 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 28747 . . . . . . 7 class norm
1510, 14cfv 6329 . . . . . 6 class (norm𝑥)
16 c2 11695 . . . . . 6 class 2
17 cexp 13442 . . . . . 6 class
1815, 16, 17co 7142 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 11301 . . . . 5 class /
2013, 18, 19co 7142 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 5113 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 5113 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1538 1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
 Colors of variables: wff setvar class This definition is referenced by:  eigvalfval  29721
 Copyright terms: Public domain W3C validator