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

Definition df-eigvec 29634
 Description: Define the eigenvector function. Theorem eleigveccl 29740 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 28740 . 2 class eigvec
2 vt . . 3 setvar 𝑡
3 chba 28700 . . . 4 class
4 cmap 8393 . . . 4 class m
53, 3, 4co 7140 . . 3 class ( ℋ ↑m ℋ)
6 vx . . . . . . . 8 setvar 𝑥
76cv 1537 . . . . . . 7 class 𝑥
82cv 1537 . . . . . . 7 class 𝑡
97, 8cfv 6334 . . . . . 6 class (𝑡𝑥)
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1537 . . . . . . 7 class 𝑧
12 csm 28702 . . . . . . 7 class ·
1311, 7, 12co 7140 . . . . . 6 class (𝑧 · 𝑥)
149, 13wceq 1538 . . . . 5 wff (𝑡𝑥) = (𝑧 · 𝑥)
15 cc 10524 . . . . 5 class
1614, 10, 15wrex 3131 . . . 4 wff 𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)
17 c0h 28716 . . . . 5 class 0
183, 17cdif 3905 . . . 4 class ( ℋ ∖ 0)
1916, 6, 18crab 3134 . . 3 class {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)}
202, 5, 19cmpt 5122 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
211, 20wceq 1538 1 wff eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})
 Colors of variables: wff setvar class This definition is referenced by:  eigvecval  29677
 Copyright terms: Public domain W3C validator