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

Definition df-eigvec 28096
 Description: Define the eigenvector function. Theorem eleigveccl 28202 shows that eigvec‘𝑇, the set of eigenvectors of Hilbert space operator 𝑇, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-eigvec eigvec = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
Distinct variable group:   𝑥,𝑡,𝑧

Detailed syntax breakdown of Definition df-eigvec
StepHypRef Expression
1 cei 27200 . 2 class eigvec
2 vt . . 3 setvar 𝑡
3 chil 27160 . . . 4 class
4 cmap 7744 . . . 4 class 𝑚
53, 3, 4co 6549 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vx . . . . . . . 8 setvar 𝑥
76cv 1474 . . . . . . 7 class 𝑥
82cv 1474 . . . . . . 7 class 𝑡
97, 8cfv 5804 . . . . . 6 class (𝑡𝑥)
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1474 . . . . . . 7 class 𝑧
12 csm 27162 . . . . . . 7 class ·
1311, 7, 12co 6549 . . . . . 6 class (𝑧 · 𝑥)
149, 13wceq 1475 . . . . 5 wff (𝑡𝑥) = (𝑧 · 𝑥)
15 cc 9813 . . . . 5 class
1614, 10, 15wrex 2897 . . . 4 wff 𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)
17 c0h 27176 . . . . 5 class 0
183, 17cdif 3537 . . . 4 class ( ℋ ∖ 0)
1916, 6, 18crab 2900 . . 3 class {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)}
202, 5, 19cmpt 4643 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
211, 20wceq 1475 1 wff eigvec = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
 Colors of variables: wff setvar class This definition is referenced by:  eigvecval  28139
 Copyright terms: Public domain W3C validator