Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-eigvec | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-eigvec | ⊢ eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cei 29300 | . 2 class eigvec | |
2 | vt | . . 3 setvar 𝑡 | |
3 | chba 29260 | . . . 4 class ℋ | |
4 | cmap 8589 | . . . 4 class ↑m | |
5 | 3, 3, 4 | co 7268 | . . 3 class ( ℋ ↑m ℋ) |
6 | vx | . . . . . . . 8 setvar 𝑥 | |
7 | 6 | cv 1540 | . . . . . . 7 class 𝑥 |
8 | 2 | cv 1540 | . . . . . . 7 class 𝑡 |
9 | 7, 8 | cfv 6430 | . . . . . 6 class (𝑡‘𝑥) |
10 | vz | . . . . . . . 8 setvar 𝑧 | |
11 | 10 | cv 1540 | . . . . . . 7 class 𝑧 |
12 | csm 29262 | . . . . . . 7 class ·ℎ | |
13 | 11, 7, 12 | co 7268 | . . . . . 6 class (𝑧 ·ℎ 𝑥) |
14 | 9, 13 | wceq 1541 | . . . . 5 wff (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥) |
15 | cc 10853 | . . . . 5 class ℂ | |
16 | 14, 10, 15 | wrex 3066 | . . . 4 wff ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥) |
17 | c0h 29276 | . . . . 5 class 0ℋ | |
18 | 3, 17 | cdif 3888 | . . . 4 class ( ℋ ∖ 0ℋ) |
19 | 16, 6, 18 | crab 3069 | . . 3 class {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)} |
20 | 2, 5, 19 | cmpt 5161 | . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)}) |
21 | 1, 20 | wceq 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 |