Definition df-spec

Description: Define the spectrum of an operator. Definition of spectrum in Halmos p. 50. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspc	$$class\mathrm{Lambda}$$
1		vt	$$setvart$$
2		chba	$$class\mathscr{H}$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4	2 2 3	co	$$class\left({\mathscr{H}}^{\mathscr{H}}\right)$$
5		vx	$$setvarx$$
6		cc	$$classℂ$$
7	1	cv	$$setvart$$
8		chod	$$class{-}_{\mathrm{op}}$$
9	5	cv	$$setvarx$$
10		chot	$$class{·}_{\mathrm{op}}$$
11		cid	$$class\mathrm{I}$$
12	11 2	cres	$$class\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)$$
13	9 12 10	co	$$class\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)$$
14	7 13 8	co	$$class\left(t{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\right)$$
15	2 2 14	wf1	$$wff\left(t{-}_{\mathrm{op}}\left(x{·}_{\mathrm{op}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right)\right):\mathscr{H}\underset{1-1}{⟶}\mathscr{H}$$
16	15	wn	$$wff\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}$$
17	16 5 6	crab	$$class\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\}$$
18	1 4 17	cmpt	$$class\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)$$
19	0 18	wceq	$$wff\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)$$