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 27880
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 26984 . 2 class Lambda
2 vt . . 3 setvar 𝑡
3 chil 26942 . . . 4 class
4 cmap 7624 . . . 4 class 𝑚
53, 3, 4co 6431 . . 3 class ( ℋ ↑𝑚 ℋ)
62cv 1473 . . . . . . 7 class 𝑡
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1473 . . . . . . . 8 class 𝑥
9 cid 4842 . . . . . . . . 9 class I
109, 3cres 4934 . . . . . . . 8 class ( I ↾ ℋ)
11 chot 26962 . . . . . . . 8 class ·op
128, 10, 11co 6431 . . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13 chod 26963 . . . . . . 7 class op
146, 12, 13co 6431 . . . . . 6 class (𝑡op (𝑥 ·op ( I ↾ ℋ)))
153, 3, 14wf1 5691 . . . . 5 wff (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
1615wn 3 . . . 4 wff ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17 cc 9693 . . . 4 class
1816, 7, 17crab 2804 . . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
192, 5, 18cmpt 4541 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
201, 19wceq 1474 1 wff Lambda = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
Colors of variables: wff setvar class
This definition is referenced by:  specval  27923
  Copyright terms: Public domain W3C validator