This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )