Metamath Proof Explorer

Theorem homval

Description: Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion homval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ B ∈ ℋ → A · op T ⁡ B = A ⋅ ℎ T ⁡ B

Proof

Step Hyp Ref Expression
1 hommval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x
2 1 fveq1d ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T ⁡ B = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x ⁡ B
3 fveq2 ⊢ x = B → T ⁡ x = T ⁡ B
4 3 oveq2d ⊢ x = B → A ⋅ ℎ T ⁡ x = A ⋅ ℎ T ⁡ B
5 eqid ⊢ x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x
6 ovex ⊢ A ⋅ ℎ T ⁡ B ∈ V
7 4 5 6 fvmpt ⊢ B ∈ ℋ → x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x ⁡ B = A ⋅ ℎ T ⁡ B
8 2 7 sylan9eq ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ B ∈ ℋ → A · op T ⁡ B = A ⋅ ℎ T ⁡ B
9 8 3impa ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ B ∈ ℋ → A · op T ⁡ B = A ⋅ ℎ T ⁡ B