Definition df-spec 28714

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

Assertion

Ref	Expression
df-spec	|- Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )

Distinct variable group:   x, t

Detailed syntax breakdown of Definition df-spec

Step	Hyp	Ref	Expression
1		cspc 27818	. 2 class Lambda
2		vt	. . 3 setvar t
3		chil 27776	. . . 4 class ~H
4		cmap 7857	. . . 4 class ^m
5	3, 3, 4	co 6650	. . 3 class ( ~H ^m ~H )
6	2	cv 1482	. . . . . . 7 class t
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1482	. . . . . . . 8 class x
9		cid 5023	. . . . . . . . 9 class _I
10	9, 3	cres 5116	. . . . . . . 8 class ( _I |` ~H )
11		chot 27796	. . . . . . . 8 class .op
12	8, 10, 11	co 6650	. . . . . . 7 class ( x .op ( _I |` ~H ) )
13		chod 27797	. . . . . . 7 class -op
14	6, 12, 13	co 6650	. . . . . 6 class ( t -op ( x .op ( _I |` ~H ) ) )
15	3, 3, 14	wf1 5885	. . . . 5 wff ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H
16	15	wn 3	. . . 4 wff -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H
17		cc 9934	. . . 4 class CC
18	16, 7, 17	crab 2916	. . 3 class { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H }
19	2, 5, 18	cmpt 4729	. 2 class ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
20	1, 19	wceq 1483	1 wff Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )

This definition is referenced by:  specval  28757