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

Definition df-spec 28698
 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 27802 . 2 class Lambda
2 vt . . 3 setvar 𝑡
3 chil 27760 . . . 4 class
4 cmap 7854 . . . 4 class 𝑚
53, 3, 4co 6647 . . 3 class ( ℋ ↑𝑚 ℋ)
62cv 1481 . . . . . . 7 class 𝑡
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1481 . . . . . . . 8 class 𝑥
9 cid 5021 . . . . . . . . 9 class I
109, 3cres 5114 . . . . . . . 8 class ( I ↾ ℋ)
11 chot 27780 . . . . . . . 8 class ·op
128, 10, 11co 6647 . . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13 chod 27781 . . . . . . 7 class op
146, 12, 13co 6647 . . . . . 6 class (𝑡op (𝑥 ·op ( I ↾ ℋ)))
153, 3, 14wf1 5883 . . . . 5 wff (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
1615wn 3 . . . 4 wff ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17 cc 9931 . . . 4 class
1816, 7, 17crab 2915 . . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
192, 5, 18cmpt 4727 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
201, 19wceq 1482 1 wff Lambda = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
 Colors of variables: wff setvar class This definition is referenced by:  specval  28741
 Copyright terms: Public domain W3C validator