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 30970
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31077 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 30076 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chba 30035 . . . 4 class
4 cmap 8803 . . . 4 class m
53, 3, 4co 7393 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1540 . . . . 5 class 𝑡
8 cei 30075 . . . . 5 class eigvec
97, 8cfv 6532 . . . 4 class (eigvec‘𝑡)
106cv 1540 . . . . . . 7 class 𝑥
1110, 7cfv 6532 . . . . . 6 class (𝑡𝑥)
12 csp 30038 . . . . . 6 class ·ih
1311, 10, 12co 7393 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 30039 . . . . . . 7 class norm
1510, 14cfv 6532 . . . . . 6 class (norm𝑥)
16 c2 12249 . . . . . 6 class 2
17 cexp 14009 . . . . . 6 class
1815, 16, 17co 7393 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 11853 . . . . 5 class /
2013, 18, 19co 7393 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 5224 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 5224 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1541 1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  31013
  Copyright terms: Public domain W3C validator