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

Definition df-spec 22451
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  =  ( t  e.  ( ~H 
^m  ~H )  |->  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H } )
Distinct variable group:    x, t

Detailed syntax breakdown of Definition df-spec
StepHypRef Expression
1 cspc 21557 . 2  class  Lambda
2 vt . . 3  set  t
3 chil 21515 . . . 4  class  ~H
4 cmap 6788 . . . 4  class  ^m
53, 3, 4co 5874 . . 3  class  ( ~H 
^m  ~H )
62cv 1631 . . . . . . 7  class  t
7 vx . . . . . . . . 9  set  x
87cv 1631 . . . . . . . 8  class  x
9 cid 4320 . . . . . . . . 9  class  _I
109, 3cres 4707 . . . . . . . 8  class  (  _I  |`  ~H )
11 chot 21535 . . . . . . . 8  class  .op
128, 10, 11co 5874 . . . . . . 7  class  ( x 
.op  (  _I  |`  ~H )
)
13 chod 21536 . . . . . . 7  class  -op
146, 12, 13co 5874 . . . . . 6  class  ( t  -op  ( x  .op  (  _I  |`  ~H )
) )
153, 3, 14wf1 5268 . . . . 5  wff  ( t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H
1615wn 3 . . . 4  wff  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H
17 cc 8751 . . . 4  class  CC
1816, 7, 17crab 2560 . . 3  class  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H }
192, 5, 18cmpt 4093 . 2  class  ( t  e.  ( ~H  ^m  ~H )  |->  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H } )
201, 19wceq 1632 1  wff  Lambda  =  ( t  e.  ( ~H 
^m  ~H )  |->  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H } )
Colors of variables: wff set class
This definition is referenced by:  specval  22494
  Copyright terms: Public domain W3C validator