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

Metamath Proof Explorer

Theorem specval

Description: The value of the spectrum of an operator. (Contributed by NM, 11-Apr-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion specval 
|- ( T : ~H --> ~H -> ( Lambda ` T ) = { x e. CC | -. ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 1 rabex 
 |-  { x e. CC | -. ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } e. _V
3 ax-hilex 
 |-  ~H e. _V
4 oveq1 
 |-  ( t = T -> ( t -op ( x .op ( _I |` ~H ) ) ) = ( T -op ( x .op ( _I |` ~H ) ) ) )
5 f1eq1 
 |-  ( ( t -op ( x .op ( _I |` ~H ) ) ) = ( T -op ( x .op ( _I |` ~H ) ) ) -> ( ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H <-> ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H ) )
6 4 5 syl 
 |-  ( t = T -> ( ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H <-> ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H ) )
7 6 notbid 
 |-  ( t = T -> ( -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H <-> -. ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H ) )
8 7 rabbidv 
 |-  ( t = T -> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } = { x e. CC | -. ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
9 df-spec 
 |-  Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
10 2 3 3 8 9 fvmptmap 
 |-  ( T : ~H --> ~H -> ( Lambda ` T ) = { x e. CC | -. ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )