Metamath Proof Explorer

Theorem hfmmval

Description: Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion hfmmval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℂ → A · fn T = x ∈ ℋ ⟼ A ⁢ T ⁡ x

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 ax-hilex ⊢ ℋ ∈ V
3 1 2 elmap ⊢ T ∈ ℂ ℋ ↔ T : ℋ ⟶ ℂ
4 oveq1 ⊢ f = A → f ⁢ g ⁡ x = A ⁢ g ⁡ x
5 4 mpteq2dv ⊢ f = A → x ∈ ℋ ⟼ f ⁢ g ⁡ x = x ∈ ℋ ⟼ A ⁢ g ⁡ x
6 fveq1 ⊢ g = T → g ⁡ x = T ⁡ x
7 6 oveq2d ⊢ g = T → A ⁢ g ⁡ x = A ⁢ T ⁡ x
8 7 mpteq2dv ⊢ g = T → x ∈ ℋ ⟼ A ⁢ g ⁡ x = x ∈ ℋ ⟼ A ⁢ T ⁡ x
9 df-hfmul ⊢ · fn = f ∈ ℂ , g ∈ ℂ ℋ ⟼ x ∈ ℋ ⟼ f ⁢ g ⁡ x
10 2 mptex ⊢ x ∈ ℋ ⟼ A ⁢ T ⁡ x ∈ V
11 5 8 9 10 ovmpo ⊢ A ∈ ℂ ∧ T ∈ ℂ ℋ → A · fn T = x ∈ ℋ ⟼ A ⁢ T ⁡ x
12 3 11 sylan2br ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℂ → A · fn T = x ∈ ℋ ⟼ A ⁢ T ⁡ x