# 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$