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