Definition df-spec 32439

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 31545	. 2 class Lambda
2		vt	. . 3 setvar 𝑡
3		chba 31503	. . . 4 class ℋ
4		cmap 8831	. . . 4 class ↑m
5	3, 3, 4	co 7412	. . 3 class ( ℋ ↑m ℋ)
6	2	cv 1569	. . . . . . 7 class 𝑡
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1569	. . . . . . . 8 class 𝑥
9		cid 5545	. . . . . . . . 9 class I
10	9, 3	cres 5653	. . . . . . . 8 class ( I ↾ ℋ)
11		chot 31523	. . . . . . . 8 class ·op
12	8, 10, 11	co 7412	. . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13		chod 31524	. . . . . . 7 class −op
14	6, 12, 13	co 7412	. . . . . 6 class (𝑡 −op (𝑥 ·op ( I ↾ ℋ)))
15	3, 3, 14	wf1 6528	. . . . 5 wff (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
16	15	wn 3	. . . 4 wff ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17		cc 11179	. . . 4 class ℂ
18	16, 7, 17	crab 3413	. . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
19	2, 5, 18	cmpt 5186	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
20	1, 19	wceq 1570	1 wff Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})

This definition is used by:  specval  32482