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	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( Lambda ‘ 𝑇 ) ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		specval	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( Lambda ‘ 𝑇 ) = { 𝑥 ∈ ℂ ∣ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )
2		ssrab2	⊢ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } ⊆ ℂ
3	1 2	eqsstrdi	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( Lambda ‘ 𝑇 ) ⊆ ℂ )