Metamath Proof Explorer

Theorem speccl

Description: The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	speccl	\|- ( T : ~H --> ~H -> ( Lambda ` T ) C_ CC )

Step	Hyp	Ref	Expression
1		specval	\|- ( T : ~H --> ~H -> ( Lambda ` T ) = { x e. CC \| -. ( T -op ( x .op ( _I \|` ~H ) ) ) : ~H -1-1-> ~H } )
2		ssrab2	\|- { x e. CC \| -. ( T -op ( x .op ( _I \|` ~H ) ) ) : ~H -1-1-> ~H } C_ CC
3	1 2	eqsstrdi	\|- ( T : ~H --> ~H -> ( Lambda ` T ) C_ CC )

Step

Hyp

Ref

Expression

 |-  ( T : ~H --> ~H -> ( Lambda ` 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 } C_ CC

1 2

 |-  ( T : ~H --> ~H -> ( Lambda ` T ) C_ CC )