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

Definition df-eigvec 27884
Description: Define the eigenvector function. Theorem eleigveccl 27990 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 26988 . 2 class eigvec
2 vt . . 3 setvar 𝑡
3 chil 26948 . . . 4 class
4 cmap 7620 . . . 4 class 𝑚
53, 3, 4co 6426 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vx . . . . . . . 8 setvar 𝑥
76cv 1473 . . . . . . 7 class 𝑥
82cv 1473 . . . . . . 7 class 𝑡
97, 8cfv 5689 . . . . . 6 class (𝑡𝑥)
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1473 . . . . . . 7 class 𝑧
12 csm 26950 . . . . . . 7 class ·
1311, 7, 12co 6426 . . . . . 6 class (𝑧 · 𝑥)
149, 13wceq 1474 . . . . 5 wff (𝑡𝑥) = (𝑧 · 𝑥)
15 cc 9689 . . . . 5 class
1614, 10, 15wrex 2801 . . . 4 wff 𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)
17 c0h 26964 . . . . 5 class 0
183, 17cdif 3441 . . . 4 class ( ℋ ∖ 0)
1916, 6, 18crab 2804 . . 3 class {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)}
202, 5, 19cmpt 4541 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
211, 20wceq 1474 1 wff eigvec = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  eigvecval  27927
  Copyright terms: Public domain W3C validator