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	|- Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspc	|- Lambda
1		vt	|- t
2		chba	|- ~H
3		cmap	|- ^m
4	2 2 3	co	|- ( ~H ^m ~H )
5		vx	|- x
6		cc	|- CC
7	1	cv	|- t
8		chod	|- -op
9	5	cv	|- x
10		chot	|- .op
11		cid	|- _I
12	11 2	cres	|- ( _I |` ~H )
13	9 12 10	co	|- ( x .op ( _I |` ~H ) )
14	7 13 8	co	|- ( t -op ( x .op ( _I |` ~H ) ) )
15	2 2 14	wf1	|- ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H
16	15	wn	|- -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H
17	16 5 6	crab	|- { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H }
18	1 4 17	cmpt	|- ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
19	0 18	wceq	|- Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )