Definition df-spec 32462

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 = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})

Distinct variable group:   𝑥,𝑡

Detailed syntax breakdown of Definition df-spec

Step	Hyp	Ref	Expression
1		cspc 31568	. 2 class Lambda
2		vt	. . 3 setvar 𝑡
3		chba 31526	. . . 4 class ℋ
4		cmap 8850	. . . 4 class ↑m
5	3, 3, 4	co 7420	. . 3 class ( ℋ ↑m ℋ)
6	2	cv 1568	. . . . . . 7 class 𝑡
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1568	. . . . . . . 8 class 𝑥
9		cid 5544	. . . . . . . . 9 class I
10	9, 3	cres 5652	. . . . . . . 8 class ( I ↾ ℋ)
11		chot 31546	. . . . . . . 8 class ·op
12	8, 10, 11	co 7420	. . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13		chod 31547	. . . . . . 7 class −op
14	6, 12, 13	co 7420	. . . . . 6 class (𝑡 −op (𝑥 ·op ( I ↾ ℋ)))
15	3, 3, 14	wf1 6535	. . . . 5 wff (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
16	15	wn 3	. . . 4 wff ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17		cc 11201	. . . 4 class ℂ
18	16, 7, 17	crab 3412	. . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
19	2, 5, 18	cmpt 5185	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
20	1, 19	wceq 1569	1 wff Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})

This definition is used by:  specval  32505