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:\mathscr{H}⟶\mathscr{H}\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	$$⊢\mathscr{H}\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({\mathscr{H}}^{\mathscr{H}}\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:\mathscr{H}⟶\mathscr{H}\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)$$