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

Definition df-spec 22435
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 21541 . 2  class  Lambda
2 vt . . 3  set  t
3 chil 21499 . . . 4  class  ~H
4 cmap 6772 . . . 4  class  ^m
53, 3, 4co 5858 . . 3  class  ( ~H 
^m  ~H )
62cv 1622 . . . . . . 7  class  t
7 vx . . . . . . . . 9  set  x
87cv 1622 . . . . . . . 8  class  x
9 cid 4304 . . . . . . . . 9  class  _I
109, 3cres 4691 . . . . . . . 8  class  (  _I  |`  ~H )
11 chot 21519 . . . . . . . 8  class  .op
128, 10, 11co 5858 . . . . . . 7  class  ( x 
.op  (  _I  |`  ~H )
)
13 chod 21520 . . . . . . 7  class  -op
146, 12, 13co 5858 . . . . . 6  class  ( t  -op  ( x  .op  (  _I  |`  ~H )
) )
153, 3, 14wf1 5252 . . . . 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 8735 . . . 4  class  CC
1816, 7, 17crab 2547 . . 3  class  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H }
192, 5, 18cmpt 4077 . 2  class  ( t  e.  ( ~H  ^m  ~H )  |->  { x  e.  CC  |  -.  (
t  -op  ( x  .op  (  _I  |`  ~H )
) ) : ~H -1-1-> ~H } )
201, 19wceq 1623 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  22478
  Copyright terms: Public domain W3C validator