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	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigval ‘ 𝑇 ) = ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( eigvec ‘ 𝑇 ) ∈ V
2	1	mptex	⊢ ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) ∈ V
3		ax-hilex	⊢ ℋ ∈ V
4		fveq2	⊢ ( 𝑡 = 𝑇 → ( eigvec ‘ 𝑡 ) = ( eigvec ‘ 𝑇 ) )
5		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
6	5	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) )
7	6	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) )
8	4 7	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑥 ∈ ( eigvec ‘ 𝑡 ) ↦ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) = ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )
9		df-eigval	⊢ eigval = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ( eigvec ‘ 𝑡 ) ↦ ( ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )
10	2 3 3 8 9	fvmptmap	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigval ‘ 𝑇 ) = ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )