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 30839
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 29945 . 2 class Lambda
2 vt . . 3 setvar ๐‘ก
3 chba 29903 . . . 4 class โ„‹
4 cmap 8772 . . . 4 class โ†‘m
53, 3, 4co 7362 . . 3 class ( โ„‹ โ†‘m โ„‹)
62cv 1541 . . . . . . 7 class ๐‘ก
7 vx . . . . . . . . 9 setvar ๐‘ฅ
87cv 1541 . . . . . . . 8 class ๐‘ฅ
9 cid 5535 . . . . . . . . 9 class I
109, 3cres 5640 . . . . . . . 8 class ( I โ†พ โ„‹)
11 chot 29923 . . . . . . . 8 class ยทop
128, 10, 11co 7362 . . . . . . 7 class (๐‘ฅ ยทop ( I โ†พ โ„‹))
13 chod 29924 . . . . . . 7 class โˆ’op
146, 12, 13co 7362 . . . . . 6 class (๐‘ก โˆ’op (๐‘ฅ ยทop ( I โ†พ โ„‹)))
153, 3, 14wf1 6498 . . . . 5 wff (๐‘ก โˆ’op (๐‘ฅ ยทop ( I โ†พ โ„‹))): โ„‹โ€“1-1โ†’ โ„‹
1615wn 3 . . . 4 wff ยฌ (๐‘ก โˆ’op (๐‘ฅ ยทop ( I โ†พ โ„‹))): โ„‹โ€“1-1โ†’ โ„‹
17 cc 11056 . . . 4 class โ„‚
1816, 7, 17crab 3410 . . 3 class {๐‘ฅ โˆˆ โ„‚ โˆฃ ยฌ (๐‘ก โˆ’op (๐‘ฅ ยทop ( I โ†พ โ„‹))): โ„‹โ€“1-1โ†’ โ„‹}
192, 5, 18cmpt 5193 . 2 class (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ โ„‚ โˆฃ ยฌ (๐‘ก โˆ’op (๐‘ฅ ยทop ( I โ†พ โ„‹))): โ„‹โ€“1-1โ†’ โ„‹})
201, 19wceq 1542 1 wff Lambda = (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ โ„‚ โˆฃ ยฌ (๐‘ก โˆ’op (๐‘ฅ ยทop ( I โ†พ โ„‹))): โ„‹โ€“1-1โ†’ โ„‹})
Colors of variables: wff setvar class
This definition is referenced by:  specval  30882
  Copyright terms: Public domain W3C validator