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:\mathscr{H}⟶\mathscr{H}\to \mathrm{Lambda}\left(T\right)\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		specval	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{Lambda}\left(T\right)=\left\{x\in ℂ|\neg \left(T{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\right):\mathscr{H}\underset{1-1}{⟶}\mathscr{H}\right\}$$
2		ssrab2	$$⊢\left\{x\in ℂ|\neg \left(T{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\right):\mathscr{H}\underset{1-1}{⟶}\mathscr{H}\right\}\subseteq ℂ$$
3	1 2	eqsstrdi	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{Lambda}\left(T\right)\subseteq ℂ$$