| Hilbert Space Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. |
| Ref | Expression |
|---|---|
| df-spec |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cspc 10254 |
. 2
| |
| 2 | chil 10212 |
. . . . 5
| |
| 3 | vt |
. . . . . 6
| |
| 4 | 3 | cv 1135 |
. . . . 5
|
| 5 | 2, 2, 4 | wf 3805 |
. . . 4
|
| 6 | vy |
. . . . . 6
| |
| 7 | 6 | cv 1135 |
. . . . 5
|
| 8 | vx |
. . . . . . . . . . 11
| |
| 9 | 8 | cv 1135 |
. . . . . . . . . 10
|
| 10 | cid 3397 |
. . . . . . . . . . 11
| |
| 11 | 10, 2 | cres 3799 |
. . . . . . . . . 10
|
| 12 | chot 10232 |
. . . . . . . . . 10
| |
| 13 | 9, 11, 12 | co 4695 |
. . . . . . . . 9
|
| 14 | chod 10233 |
. . . . . . . . 9
| |
| 15 | 4, 13, 14 | co 4695 |
. . . . . . . 8
|
| 16 | 2, 2, 15 | wf1 3806 |
. . . . . . 7
|
| 17 | 16 | wn 2 |
. . . . . 6
|
| 18 | cc 6180 |
. . . . . 6
| |
| 19 | 17, 8, 18 | crab 1942 |
. . . . 5
|
| 20 | 7, 19 | wceq 1136 |
. . . 4
|
| 21 | 5, 20 | wa 239 |
. . 3
|
| 22 | 21, 3, 6 | copab 3213 |
. 2
|
| 23 | 1, 22 | wceq 1136 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: specval 11253 |