Definition df-spec 11210

Description: Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50.

Assertion

Ref	Expression
df-spec	|- Lambda = {<.t, y>. | (t:~H-->~H /\ y = {x e. CC | -. (t -op (x .op (_I |` ~H))):~H-1-1->~H})}

Distinct variable group:   x,t,y

Detailed syntax breakdown of Definition df-spec

Step	Hyp	Ref	Expression
1		cspc 10254	. 2 class Lambda
2		chil 10212	. . . . 5 class ~H
3		vt	. . . . . 6 set t
4	3	cv 1135	. . . . 5 class t
5	2, 2, 4	wf 3805	. . . 4 wff t:~H-->~H
6		vy	. . . . . 6 set y
7	6	cv 1135	. . . . 5 class y
8		vx	. . . . . . . . . . 11 set x
9	8	cv 1135	. . . . . . . . . 10 class x
10		cid 3397	. . . . . . . . . . 11 class _I
11	10, 2	cres 3799	. . . . . . . . . 10 class (_I |` ~H)
12		chot 10232	. . . . . . . . . 10 class .op
13	9, 11, 12	co 4695	. . . . . . . . 9 class (x .op (_I |` ~H))
14		chod 10233	. . . . . . . . 9 class -op
15	4, 13, 14	co 4695	. . . . . . . 8 class (t -op (x .op (_I |` ~H)))
16	2, 2, 15	wf1 3806	. . . . . . 7 wff (t -op (x .op (_I |` ~H))):~H-1-1->~H
17	16	wn 2	. . . . . 6 wff -. (t -op (x .op (_I |` ~H))):~H-1-1->~H
18		cc 6180	. . . . . 6 class CC
19	17, 8, 18	crab 1942	. . . . 5 class {x e. CC | -. (t -op (x .op (_I |` ~H))):~H-1-1->~H}
20	7, 19	wceq 1136	. . . 4 wff y = {x e. CC | -. (t -op (x .op (_I |` ~H))):~H-1-1->~H}
21	5, 20	wa 239	. . 3 wff (t:~H-->~H /\ y = {x e. CC | -. (t -op (x .op (_I |` ~H))):~H-1-1->~H})
22	21, 3, 6	copab 3213	. 2 class {<.t, y>. | (t:~H-->~H /\ y = {x e. CC | -. (t -op (x .op (_I |` ~H))):~H-1-1->~H})}
23	1, 22	wceq 1136	1 wff Lambda = {<.t, y>. | (t:~H-->~H /\ y = {x e. CC | -. (t -op (x .op (_I |` ~H))):~H-1-1->~H})}

This definition is referenced by:  specval 11253

Copyright terms: Public domain