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 ) ) )