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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 eigvalfval ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( eigval ‘ 𝑇 ) = ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) )
2 1 fveq1d ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) ‘ 𝐴 ) )
3 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝐴 ) )
4 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
5 3 4 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) )
6 fveq2 ⊢ ( 𝑥 = 𝐴 → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 𝐴 ) )
7 6 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( normℎ ‘ 𝑥 ) ↑ 2 ) = ( ( normℎ ‘ 𝐴 ) ↑ 2 ) )
8 5 7 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) )
9 eqid ⊢ ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) = ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) )
10 ovex ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) ∈ V
11 8 9 10 fvmpt ⊢ ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) → ( ( 𝑥 ∈ ( eigvec ‘ 𝑇 ) ↦ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) / ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) ) ‘ 𝐴 ) = ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) )
12 2 11 sylan9eq ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) = ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) / ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) )