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 30838
Description: Define the eigenvalue function. The range of eigvalβ€˜π‘‡ is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 30945 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 29944 . 2 class eigval
2 vt . . 3 setvar 𝑑
3 chba 29903 . . . 4 class β„‹
4 cmap 8768 . . . 4 class ↑m
53, 3, 4co 7358 . . 3 class ( β„‹ ↑m β„‹)
6 vx . . . 4 setvar π‘₯
72cv 1541 . . . . 5 class 𝑑
8 cei 29943 . . . . 5 class eigvec
97, 8cfv 6497 . . . 4 class (eigvecβ€˜π‘‘)
106cv 1541 . . . . . . 7 class π‘₯
1110, 7cfv 6497 . . . . . 6 class (π‘‘β€˜π‘₯)
12 csp 29906 . . . . . 6 class Β·ih
1311, 10, 12co 7358 . . . . 5 class ((π‘‘β€˜π‘₯) Β·ih π‘₯)
14 cno 29907 . . . . . . 7 class normβ„Ž
1510, 14cfv 6497 . . . . . 6 class (normβ„Žβ€˜π‘₯)
16 c2 12213 . . . . . 6 class 2
17 cexp 13973 . . . . . 6 class ↑
1815, 16, 17co 7358 . . . . 5 class ((normβ„Žβ€˜π‘₯)↑2)
19 cdiv 11817 . . . . 5 class /
2013, 18, 19co 7358 . . . 4 class (((π‘‘β€˜π‘₯) Β·ih π‘₯) / ((normβ„Žβ€˜π‘₯)↑2))
216, 9, 20cmpt 5189 . . 3 class (π‘₯ ∈ (eigvecβ€˜π‘‘) ↦ (((π‘‘β€˜π‘₯) Β·ih π‘₯) / ((normβ„Žβ€˜π‘₯)↑2)))
222, 5, 21cmpt 5189 . 2 class (𝑑 ∈ ( β„‹ ↑m β„‹) ↦ (π‘₯ ∈ (eigvecβ€˜π‘‘) ↦ (((π‘‘β€˜π‘₯) Β·ih π‘₯) / ((normβ„Žβ€˜π‘₯)↑2))))
231, 22wceq 1542 1 wff eigval = (𝑑 ∈ ( β„‹ ↑m β„‹) ↦ (π‘₯ ∈ (eigvecβ€˜π‘‘) ↦ (((π‘‘β€˜π‘₯) Β·ih π‘₯) / ((normβ„Žβ€˜π‘₯)↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  eigvalfval  30881
  Copyright terms: Public domain W3C validator