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 ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A = T ⁡ A ⋅ ih A norm ℎ ⁡ A 2

Proof

Step Hyp Ref Expression
1 eigvalfval ⊢ T : ℋ ⟶ ℋ → eigval ⁡ T = x ∈ eigvec ⁡ T ⟼ T ⁡ x ⋅ ih x norm ℎ ⁡ x 2
2 1 fveq1d ⊢ T : ℋ ⟶ ℋ → eigval ⁡ T ⁡ A = x ∈ eigvec ⁡ T ⟼ T ⁡ x ⋅ ih x norm ℎ ⁡ x 2 ⁡ A
3 fveq2 ⊢ x = A → T ⁡ x = T ⁡ A
4 id ⊢ x = A → x = A
5 3 4 oveq12d ⊢ x = A → T ⁡ x ⋅ ih x = T ⁡ A ⋅ ih A
6 fveq2 ⊢ x = A → norm ℎ ⁡ x = norm ℎ ⁡ A
7 6 oveq1d ⊢ x = A → norm ℎ ⁡ x 2 = norm ℎ ⁡ A 2
8 5 7 oveq12d ⊢ x = A → T ⁡ x ⋅ ih x norm ℎ ⁡ x 2 = T ⁡ A ⋅ ih A norm ℎ ⁡ A 2
9 eqid ⊢ x ∈ eigvec ⁡ T ⟼ T ⁡ x ⋅ ih x norm ℎ ⁡ x 2 = x ∈ eigvec ⁡ T ⟼ T ⁡ x ⋅ ih x norm ℎ ⁡ x 2
10 ovex ⊢ T ⁡ A ⋅ ih A norm ℎ ⁡ A 2 ∈ V
11 8 9 10 fvmpt ⊢ A ∈ eigvec ⁡ T → x ∈ eigvec ⁡ T ⟼ T ⁡ x ⋅ ih x norm ℎ ⁡ x 2 ⁡ A = T ⁡ A ⋅ ih A norm ℎ ⁡ A 2
12 2 11 sylan9eq ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A = T ⁡ A ⋅ ih A norm ℎ ⁡ A 2