# 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 ${⊢}{T}:ℋ⟶ℋ\to \mathrm{Lambda}\left({T}\right)=\left\{{x}\in ℂ|¬\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right\}$

### Proof

Step Hyp Ref Expression
1 cnex ${⊢}ℂ\in \mathrm{V}$
2 1 rabex ${⊢}\left\{{x}\in ℂ|¬\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right\}\in \mathrm{V}$
3 ax-hilex ${⊢}ℋ\in \mathrm{V}$
4 oveq1 ${⊢}{t}={T}\to {t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)={T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)$
5 f1eq1 ${⊢}{t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)={T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\to \left(\left({t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ↔\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right)$
6 4 5 syl ${⊢}{t}={T}\to \left(\left({t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ↔\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right)$
7 6 notbid ${⊢}{t}={T}\to \left(¬\left({t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ↔¬\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right)$
8 7 rabbidv ${⊢}{t}={T}\to \left\{{x}\in ℂ|¬\left({t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right\}=\left\{{x}\in ℂ|¬\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right\}$
9 df-spec ${⊢}\mathrm{Lambda}=\left({t}\in \left({ℋ}^{ℋ}\right)⟼\left\{{x}\in ℂ|¬\left({t}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right\}\right)$
10 2 3 3 8 9 fvmptmap ${⊢}{T}:ℋ⟶ℋ\to \mathrm{Lambda}\left({T}\right)=\left\{{x}\in ℂ|¬\left({T}{-}_{\mathrm{op}}\left({x}{·}_{\mathrm{op}}\left({\mathrm{I}↾}_{ℋ}\right)\right)\right):ℋ\underset{1-1}{⟶}ℋ\right\}$