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 29054
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 28158 . 2 class Lambda
2 vt . . 3 setvar 𝑡
3 chil 28116 . . . 4 class
4 cmap 8009 . . . 4 class 𝑚
53, 3, 4co 6793 . . 3 class ( ℋ ↑𝑚 ℋ)
62cv 1630 . . . . . . 7 class 𝑡
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1630 . . . . . . . 8 class 𝑥
9 cid 5156 . . . . . . . . 9 class I
109, 3cres 5251 . . . . . . . 8 class ( I ↾ ℋ)
11 chot 28136 . . . . . . . 8 class ·op
128, 10, 11co 6793 . . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13 chod 28137 . . . . . . 7 class op
146, 12, 13co 6793 . . . . . 6 class (𝑡op (𝑥 ·op ( I ↾ ℋ)))
153, 3, 14wf1 6028 . . . . 5 wff (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
1615wn 3 . . . 4 wff ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17 cc 10136 . . . 4 class
1816, 7, 17crab 3065 . . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
192, 5, 18cmpt 4863 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
201, 19wceq 1631 1 wff Lambda = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
Colors of variables: wff setvar class
This definition is referenced by:  specval  29097
  Copyright terms: Public domain W3C validator