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