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: ℋ –→ ℋ ⋀ y = {x ∈ ℂ∣ ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ })}

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 ℋ
3		vt	. . . . . 6 set t
4	3	cv 952	. . . . 5 class t
5	2, 2, 4	wf 3168	. . . 4 wff t: ℋ –→ ℋ
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 ↾ ℋ )
12		chot 8747	. . . . . . . . . 10 class ·op
13	9, 11, 12	co 3948	. . . . . . . . 9 class (x ·op (I ↾ ℋ ))
14		chod 8748	. . . . . . . . 9 class −op
15	4, 13, 14	co 3948	. . . . . . . 8 class (t −op (x ·op (I ↾ ℋ )))
16	2, 2, 15	wf1 3169	. . . . . . 7 wff (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ
17	16	wn 2	. . . . . 6 wff ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ
18		cc 5204	. . . . . 6 class ℂ
19	17, 8, 18	crab 1640	. . . . 5 class {x ∈ ℂ∣ ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ }
20	7, 19	wceq 953	. . . 4 wff y = {x ∈ ℂ∣ ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ }
21	5, 20	wa 223	. . 3 wff (t: ℋ –→ ℋ ⋀ y = {x ∈ ℂ∣ ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ })
22	21, 3, 6	copab 2656	. 2 class {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {x ∈ ℂ∣ ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ })}
23	1, 22	wceq 953	1 wff Lambda = {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {x ∈ ℂ∣ ¬ (t −op (x ·op (I ↾ ℋ ))): ℋ –1-1→ ℋ })}

This definition is referenced by:  specvalt 9741

Copyright terms: Public domain