# Metamath Proof Explorer

## Theorem eigvalfval

Description: The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigvalfval ${⊢}{T}:ℋ⟶ℋ\to \mathrm{eigval}\left({T}\right)=\left({x}\in \mathrm{eigvec}\left({T}\right)⟼\frac{{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}\right)$

### Proof

Step Hyp Ref Expression
1 fvex ${⊢}\mathrm{eigvec}\left({T}\right)\in \mathrm{V}$
2 1 mptex ${⊢}\left({x}\in \mathrm{eigvec}\left({T}\right)⟼\frac{{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}\right)\in \mathrm{V}$
3 ax-hilex ${⊢}ℋ\in \mathrm{V}$
4 fveq2 ${⊢}{t}={T}\to \mathrm{eigvec}\left({t}\right)=\mathrm{eigvec}\left({T}\right)$
5 fveq1 ${⊢}{t}={T}\to {t}\left({x}\right)={T}\left({x}\right)$
6 5 oveq1d ${⊢}{t}={T}\to {t}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
7 6 oveq1d ${⊢}{t}={T}\to \frac{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}=\frac{{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}$
8 4 7 mpteq12dv ${⊢}{t}={T}\to \left({x}\in \mathrm{eigvec}\left({t}\right)⟼\frac{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}\right)=\left({x}\in \mathrm{eigvec}\left({T}\right)⟼\frac{{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}\right)$
9 df-eigval ${⊢}\mathrm{eigval}=\left({t}\in \left({ℋ}^{ℋ}\right)⟼\left({x}\in \mathrm{eigvec}\left({t}\right)⟼\frac{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}\right)\right)$
10 2 3 3 8 9 fvmptmap ${⊢}{T}:ℋ⟶ℋ\to \mathrm{eigval}\left({T}\right)=\left({x}\in \mathrm{eigvec}\left({T}\right)⟼\frac{{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}}{{{norm}_{ℎ}\left({x}\right)}^{2}}\right)$