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

Metamath Proof Explorer

Theorem specval

Description: The value of the spectrum of an operator. (Contributed by NM, 11-Apr-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion specval ( 𝑇 : ℋ ⟶ ℋ → ( Lambda ‘ 𝑇 ) = { 𝑥 ∈ ℂ ∣ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 1 rabex ⊢ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } ∈ V
3 ax-hilex ⊢ ℋ ∈ V
4 oveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) = ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) )
5 f1eq1 ⊢ ( ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) = ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) → ( ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ ↔ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ ) )
6 4 5 syl ⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ ↔ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ ) )
7 6 notbid ⊢ ( 𝑡 = 𝑇 → ( ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ ↔ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ ) )
8 7 rabbidv ⊢ ( 𝑡 = 𝑇 → { 𝑥 ∈ ℂ ∣ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } = { 𝑥 ∈ ℂ ∣ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )
9 df-spec ⊢ Lambda = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ℂ ∣ ¬ ( 𝑡 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )
10 2 3 3 8 9 fvmptmap ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( Lambda ‘ 𝑇 ) = { 𝑥 ∈ ℂ ∣ ¬ ( 𝑇 −op ( 𝑥 ·op ( I ↾ ℋ ) ) ) : ℋ –1-1→ ℋ } )