Definition df-spec

Description: Define the spectrum of an operator. Definition of spectrum in Halmos p. 50. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-spec	⊢ Lambda = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspc	⊢ Lambda
1		vt	⊢ 𝑡
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4	2 2 3	co	⊢ ( ℋ ↑m ℋ )
5		vx	⊢ 𝑥
6		cc	⊢ ℂ
7	1	cv	⊢ 𝑡
8		chod	⊢ −op
9	5	cv	⊢ 𝑥
10		chot	⊢ ·op
11		cid	⊢ I
12	11 2	cres	⊢ ( I ↾ ℋ )
13	9 12 10	co	⊢ ( 𝑥 ·op ( I ↾ ℋ ) )
14	7 13 8	co	⊢ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) )
15	2 2 14	wf1	⊢ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ
16	15	wn	⊢ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ
17	16 5 6	crab	⊢ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ }
18	1 4 17	cmpt	⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )
19	0 18	wceq	⊢ Lambda = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )