Definition df-spec 9698

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 8769	. 2 class Lambda
2		chil 8727	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 952	. . . . 5 class t
5	2, 2, 4	wf 3168	. . . 4 wff t:H~-->H~
6		vy	. . . . . 6 set y
7	6	cv 952	. . . . 5 class y
8		vx	. . . . . . . . . . 11 set x
9	8	cv 952	. . . . . . . . . 10 class x
10		cid 2820	. . . . . . . . . . 11 class I
11	10, 2	cres 3162	. . . . . . . . . 10 class (I |` H~)
12		chot 8747	. . . . . . . . . 10 class .op
13	9, 11, 12	co 3948	. . . . . . . . 9 class (x .op (I |` H~))
14		chod 8748	. . . . . . . . 9 class -op
15	4, 13, 14	co 3948	. . . . . . . 8 class (t -op (x .op (I |` H~)))
16	2, 2, 15	wf1 3169	. . . . . . 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 5204	. . . . . 6 class CC
19	17, 8, 18	crab 1640	. . . . 5 class {x e. CC | -. (t -op (x .op (I |` H~))):H~-1-1->H~}
20	7, 19	wceq 953	. . . 4 wff y = {x e. CC | -. (t -op (x .op (I |` H~))):H~-1-1->H~}
21	5, 20	wa 223	. . 3 wff (t:H~-->H~ /\ y = {x e. CC | -. (t -op (x .op (I |` H~))):H~-1-1->H~})
22	21, 3, 6	copab 2656	. 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 953	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:  specvalt 9741

Copyright terms: Public domain