Theorem eigvalval

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

	Ref	Expression
Assertion	eigvalval	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathrm{eigvec}\left(T\right)\right)\to \mathrm{eigval}\left(T\right)\left(A\right)=\frac{T\left(A\right){\cdot }_{\mathrm{ih}}A}{{{norm}_{ℎ}\left(A\right)}^2}$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	fveq1d	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{eigval}\left(T\right)\left(A\right)=\left(x\in \mathrm{eigvec}\left(T\right)⟼\frac{T\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}\right)\left(A\right)$$
3		fveq2	$$⊢x=A\to T\left(x\right)=T\left(A\right)$$
4		id	$$⊢x=A\to x=A$$
5	3 4	oveq12d	$$⊢x=A\to T\left(x\right){\cdot }_{\mathrm{ih}}x=T\left(A\right){\cdot }_{\mathrm{ih}}A$$
6		fveq2	$$⊢x=A\to {norm}_{ℎ}\left(x\right)={norm}_{ℎ}\left(A\right)$$
7	6	oveq1d	$$⊢x=A\to {{norm}_{ℎ}\left(x\right)}^2={{norm}_{ℎ}\left(A\right)}^2$$
8	5 7	oveq12d	$$⊢x=A\to \frac{T\left(x\right){\cdot }_{\mathrm{ih}}x}{{{norm}_{ℎ}\left(x\right)}^2}=\frac{T\left(A\right){\cdot }_{\mathrm{ih}}A}{{{norm}_{ℎ}\left(A\right)}^2}$$
9		eqid	$$⊢\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)$$
10		ovex	$$⊢\frac{T\left(A\right){\cdot }_{\mathrm{ih}}A}{{{norm}_{ℎ}\left(A\right)}^2}\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢A\in \mathrm{eigvec}\left(T\right)\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(A\right)=\frac{T\left(A\right){\cdot }_{\mathrm{ih}}A}{{{norm}_{ℎ}\left(A\right)}^2}$$
12	2 11	sylan9eq	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathrm{eigvec}\left(T\right)\right)\to \mathrm{eigval}\left(T\right)\left(A\right)=\frac{T\left(A\right){\cdot }_{\mathrm{ih}}A}{{{norm}_{ℎ}\left(A\right)}^2}$$