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 29935
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 30042 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 29041 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chba 29000 . . . 4 class
4 cmap 8508 . . . 4 class m
53, 3, 4co 7213 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1542 . . . . 5 class 𝑡
8 cei 29040 . . . . 5 class eigvec
97, 8cfv 6380 . . . 4 class (eigvec‘𝑡)
106cv 1542 . . . . . . 7 class 𝑥
1110, 7cfv 6380 . . . . . 6 class (𝑡𝑥)
12 csp 29003 . . . . . 6 class ·ih
1311, 10, 12co 7213 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 29004 . . . . . . 7 class norm
1510, 14cfv 6380 . . . . . 6 class (norm𝑥)
16 c2 11885 . . . . . 6 class 2
17 cexp 13635 . . . . . 6 class
1815, 16, 17co 7213 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 11489 . . . . 5 class /
2013, 18, 19co 7213 . . . 4 class (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))
216, 9, 20cmpt 5135 . . 3 class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2)))
222, 5, 21cmpt 5135 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
231, 22wceq 1543 1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  29978
  Copyright terms: Public domain W3C validator