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 30194
Description: Define the eigenvector function. Theorem eleigveccl 30300 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 = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
Distinct variable group:   𝑥,𝑡,𝑧

Detailed syntax breakdown of Definition df-eigvec
StepHypRef Expression
1 cei 29300 . 2 class eigvec
2 vt . . 3 setvar 𝑡
3 chba 29260 . . . 4 class
4 cmap 8589 . . . 4 class m
53, 3, 4co 7268 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . . . . . 8 setvar 𝑥
76cv 1540 . . . . . . 7 class 𝑥
82cv 1540 . . . . . . 7 class 𝑡
97, 8cfv 6430 . . . . . 6 class (𝑡𝑥)
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1540 . . . . . . 7 class 𝑧
12 csm 29262 . . . . . . 7 class ·
1311, 7, 12co 7268 . . . . . 6 class (𝑧 · 𝑥)
149, 13wceq 1541 . . . . 5 wff (𝑡𝑥) = (𝑧 · 𝑥)
15 cc 10853 . . . . 5 class
1614, 10, 15wrex 3066 . . . 4 wff 𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)
17 c0h 29276 . . . . 5 class 0
183, 17cdif 3888 . . . 4 class ( ℋ ∖ 0)
1916, 6, 18crab 3069 . . 3 class {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)}
202, 5, 19cmpt 5161 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
211, 20wceq 1541 1 wff eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  eigvecval  30237
  Copyright terms: Public domain W3C validator