Metamath Proof Explorer


Definition df-spec

Description: Define the spectrum of an operator. Definition of spectrum in Halmos p. 50. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion df-spec
|- Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cspc
 |-  Lambda
1 vt
 |-  t
2 chba
 |-  ~H
3 cmap
 |-  ^m
4 2 2 3 co
 |-  ( ~H ^m ~H )
5 vx
 |-  x
6 cc
 |-  CC
7 1 cv
 |-  t
8 chod
 |-  -op
9 5 cv
 |-  x
10 chot
 |-  .op
11 cid
 |-  _I
12 11 2 cres
 |-  ( _I |` ~H )
13 9 12 10 co
 |-  ( x .op ( _I |` ~H ) )
14 7 13 8 co
 |-  ( t -op ( x .op ( _I |` ~H ) ) )
15 2 2 14 wf1
 |-  ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H
16 15 wn
 |-  -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H
17 16 5 6 crab
 |-  { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H }
18 1 4 17 cmpt
 |-  ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
19 0 18 wceq
 |-  Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )