# Metamath Proof Explorer

## Theorem hfmval

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

Ref Expression
Assertion hfmval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\wedge {B}\in ℋ\right)\to \left({A}{·}_{\mathrm{fn}}{T}\right)\left({B}\right)={A}{T}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 hfmmval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\right)\to {A}{·}_{\mathrm{fn}}{T}=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)$
2 1 fveq1d ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\right)\to \left({A}{·}_{\mathrm{fn}}{T}\right)\left({B}\right)=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)\left({B}\right)$
3 fveq2 ${⊢}{x}={B}\to {T}\left({x}\right)={T}\left({B}\right)$
4 3 oveq2d ${⊢}{x}={B}\to {A}{T}\left({x}\right)={A}{T}\left({B}\right)$
5 eqid ${⊢}\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)$
6 ovex ${⊢}{A}{T}\left({B}\right)\in \mathrm{V}$
7 4 5 6 fvmpt ${⊢}{B}\in ℋ\to \left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)\left({B}\right)={A}{T}\left({B}\right)$
8 2 7 sylan9eq ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\right)\wedge {B}\in ℋ\right)\to \left({A}{·}_{\mathrm{fn}}{T}\right)\left({B}\right)={A}{T}\left({B}\right)$
9 8 3impa ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\wedge {B}\in ℋ\right)\to \left({A}{·}_{\mathrm{fn}}{T}\right)\left({B}\right)={A}{T}\left({B}\right)$