This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ ℋ } )