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:\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\}$$

Proof

Step	Hyp	Ref	Expression
1		cnex	$$⊢ℂ\in \mathrm{V}$$
2	1	rabex	$$⊢\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\}\in \mathrm{V}$$
3		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
4		oveq1	$$⊢t=T\to t{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)=T{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)$$
5		f1eq1	$$⊢t{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)=T{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\to \left(\left(t{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\right):\mathscr{H}\underset{1-1}{⟶}\mathscr{H}\leftrightarrow \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)$$
6	4 5	syl	$$⊢t=T\to \left(\left(t{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\right):\mathscr{H}\underset{1-1}{⟶}\mathscr{H}\leftrightarrow \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)$$
7	6	notbid	$$⊢t=T\to \left(\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}\leftrightarrow \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)$$
8	7	rabbidv	$$⊢t=T\to \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\}=\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\}$$
9		df-spec	$$⊢\mathrm{Lambda}=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\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\}\right)$$
10	2 3 3 8 9	fvmptmap	$$⊢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\}$$