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

Definition df-spec 23311
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 22417 . 2  class  Lambda
2 vt . . 3  set  t
3 chil 22375 . . . 4  class  ~H
4 cmap 6977 . . . 4  class  ^m
53, 3, 4co 6040 . . 3  class  ( ~H 
^m  ~H )
62cv 1648 . . . . . . 7  class  t
7 vx . . . . . . . . 9  set  x
87cv 1648 . . . . . . . 8  class  x
9 cid 4453 . . . . . . . . 9  class  _I
109, 3cres 4839 . . . . . . . 8  class  (  _I  |`  ~H )
11 chot 22395 . . . . . . . 8  class  .op
128, 10, 11co 6040 . . . . . . 7  class  ( x 
.op  (  _I  |`  ~H )
)
13 chod 22396 . . . . . . 7  class  -op
146, 12, 13co 6040 . . . . . 6  class  ( t  -op  ( x  .op  (  _I  |`  ~H )
) )
153, 3, 14wf1 5410 . . . . 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 8944 . . . 4  class  CC
1816, 7, 17crab 2670 . . 3  class  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H }
192, 5, 18cmpt 4226 . 2  class  ( t  e.  ( ~H  ^m  ~H )  |->  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H } )
201, 19wceq 1649 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  23354
  Copyright terms: Public domain W3C validator