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

Definition df-spec 29642
 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 = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
Distinct variable group:   𝑥,𝑡

Detailed syntax breakdown of Definition df-spec
StepHypRef Expression
1 cspc 28748 . 2 class Lambda
2 vt . . 3 setvar 𝑡
3 chba 28706 . . . 4 class
4 cmap 8393 . . . 4 class m
53, 3, 4co 7139 . . 3 class ( ℋ ↑m ℋ)
62cv 1537 . . . . . . 7 class 𝑡
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1537 . . . . . . . 8 class 𝑥
9 cid 5427 . . . . . . . . 9 class I
109, 3cres 5525 . . . . . . . 8 class ( I ↾ ℋ)
11 chot 28726 . . . . . . . 8 class ·op
128, 10, 11co 7139 . . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13 chod 28727 . . . . . . 7 class op
146, 12, 13co 7139 . . . . . 6 class (𝑡op (𝑥 ·op ( I ↾ ℋ)))
153, 3, 14wf1 6325 . . . . 5 wff (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
1615wn 3 . . . 4 wff ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17 cc 10528 . . . 4 class
1816, 7, 17crab 3113 . . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
192, 5, 18cmpt 5113 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
201, 19wceq 1538 1 wff Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
 Colors of variables: wff setvar class This definition is referenced by:  specval  29685
 Copyright terms: Public domain W3C validator