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

Definition df-spec 28098
Description: Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-spec Lambda = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
Distinct variable group:   𝑥,𝑡

Detailed syntax breakdown of Definition df-spec
StepHypRef Expression
1 cspc 27202 . 2 class Lambda
2 vt . . 3 setvar 𝑡
3 chil 27160 . . . 4 class
4 cmap 7744 . . . 4 class 𝑚
53, 3, 4co 6549 . . 3 class ( ℋ ↑𝑚 ℋ)
62cv 1474 . . . . . . 7 class 𝑡
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1474 . . . . . . . 8 class 𝑥
9 cid 4948 . . . . . . . . 9 class I
109, 3cres 5040 . . . . . . . 8 class ( I ↾ ℋ)
11 chot 27180 . . . . . . . 8 class ·op
128, 10, 11co 6549 . . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13 chod 27181 . . . . . . 7 class op
146, 12, 13co 6549 . . . . . 6 class (𝑡op (𝑥 ·op ( I ↾ ℋ)))
153, 3, 14wf1 5801 . . . . 5 wff (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
1615wn 3 . . . 4 wff ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17 cc 9813 . . . 4 class
1816, 7, 17crab 2900 . . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
192, 5, 18cmpt 4643 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
201, 19wceq 1475 1 wff Lambda = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
Colors of variables: wff setvar class
This definition is referenced by:  specval  28141
  Copyright terms: Public domain W3C validator