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 31874
Description: Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31981 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 30980 . 2 class eigval
2 vt . . 3 setvar 𝑡
3 chba 30939 . . . 4 class
4 cmap 8867 . . . 4 class m
53, 3, 4co 7432 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . 4 setvar 𝑥
72cv 1538 . . . . 5 class 𝑡
8 cei 30979 . . . . 5 class eigvec
97, 8cfv 6560 . . . 4 class (eigvec‘𝑡)
106cv 1538 . . . . . . 7 class 𝑥
1110, 7cfv 6560 . . . . . 6 class (𝑡𝑥)
12 csp 30942 . . . . . 6 class ·ih
1311, 10, 12co 7432 . . . . 5 class ((𝑡𝑥) ·ih 𝑥)
14 cno 30943 . . . . . . 7 class norm
1510, 14cfv 6560 . . . . . 6 class (norm𝑥)
16 c2 12322 . . . . . 6 class 2
17 cexp 14103 . . . . . 6 class
1815, 16, 17co 7432 . . . . 5 class ((norm𝑥)↑2)
19 cdiv 11921 . . . . 5 class /
2013, 18, 19co 7432 . . . 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 1539 1 wff eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  31917
  Copyright terms: Public domain W3C validator