Definition df-spec 31875

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 30981	. 2 class Lambda
2		vt	. . 3 setvar 𝑡
3		chba 30939	. . . 4 class ℋ
4		cmap 8867	. . . 4 class ↑m
5	3, 3, 4	co 7432	. . 3 class ( ℋ ↑m ℋ)
6	2	cv 1538	. . . . . . 7 class 𝑡
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1538	. . . . . . . 8 class 𝑥
9		cid 5576	. . . . . . . . 9 class I
10	9, 3	cres 5686	. . . . . . . 8 class ( I ↾ ℋ)
11		chot 30959	. . . . . . . 8 class ·op
12	8, 10, 11	co 7432	. . . . . . 7 class (𝑥 ·op ( I ↾ ℋ))
13		chod 30960	. . . . . . 7 class −op
14	6, 12, 13	co 7432	. . . . . 6 class (𝑡 −op (𝑥 ·op ( I ↾ ℋ)))
15	3, 3, 14	wf1 6557	. . . . 5 wff (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
16	15	wn 3	. . . 4 wff ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ
17		cc 11154	. . . 4 class ℂ
18	16, 7, 17	crab 3435	. . 3 class {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}
19	2, 5, 18	cmpt 5224	. 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
20	1, 19	wceq 1539	1 wff Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})

This definition is referenced by:  specval  31918