# Metamath Proof Explorer

## Theorem eigvecval

Description: The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion eigvecval ${⊢}{T}:ℋ⟶ℋ\to \mathrm{eigvec}\left({T}\right)=\left\{{x}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right\}$

### Proof

Step Hyp Ref Expression
1 ax-hilex ${⊢}ℋ\in \mathrm{V}$
2 difexg ${⊢}ℋ\in \mathrm{V}\to ℋ\setminus {0}_{ℋ}\in \mathrm{V}$
3 1 2 ax-mp ${⊢}ℋ\setminus {0}_{ℋ}\in \mathrm{V}$
4 3 rabex ${⊢}\left\{{x}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right\}\in \mathrm{V}$
5 fveq1 ${⊢}{t}={T}\to {t}\left({x}\right)={T}\left({x}\right)$
6 5 eqeq1d ${⊢}{t}={T}\to \left({t}\left({x}\right)={y}{\cdot }_{ℎ}{x}↔{T}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right)$
7 6 rexbidv ${⊢}{t}={T}\to \left(\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{t}\left({x}\right)={y}{\cdot }_{ℎ}{x}↔\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right)$
8 7 rabbidv ${⊢}{t}={T}\to \left\{{x}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{t}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right\}=\left\{{x}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right\}$
9 df-eigvec ${⊢}\mathrm{eigvec}=\left({t}\in \left({ℋ}^{ℋ}\right)⟼\left\{{x}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{t}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right\}\right)$
10 4 1 1 8 9 fvmptmap ${⊢}{T}:ℋ⟶ℋ\to \mathrm{eigvec}\left({T}\right)=\left\{{x}\in \left(ℋ\setminus {0}_{ℋ}\right)|\exists {y}\in ℂ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={y}{\cdot }_{ℎ}{x}\right\}$