This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑇 : ℋ ⟶ ℋ → ( 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 ) ) ) )