# 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 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\right)\to {A}{·}_{\mathrm{fn}}{T}=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cnex ${⊢}ℂ\in \mathrm{V}$
2 ax-hilex ${⊢}ℋ\in \mathrm{V}$
3 1 2 elmap ${⊢}{T}\in \left({ℂ}^{ℋ}\right)↔{T}:ℋ⟶ℂ$
4 oveq1 ${⊢}{f}={A}\to {f}{g}\left({x}\right)={A}{g}\left({x}\right)$
5 4 mpteq2dv ${⊢}{f}={A}\to \left({x}\in ℋ⟼{f}{g}\left({x}\right)\right)=\left({x}\in ℋ⟼{A}{g}\left({x}\right)\right)$
6 fveq1 ${⊢}{g}={T}\to {g}\left({x}\right)={T}\left({x}\right)$
7 6 oveq2d ${⊢}{g}={T}\to {A}{g}\left({x}\right)={A}{T}\left({x}\right)$
8 7 mpteq2dv ${⊢}{g}={T}\to \left({x}\in ℋ⟼{A}{g}\left({x}\right)\right)=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)$
9 df-hfmul ${⊢}{·}_{\mathrm{fn}}=\left({f}\in ℂ,{g}\in \left({ℂ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}{g}\left({x}\right)\right)\right)$
10 2 mptex ${⊢}\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)\in \mathrm{V}$
11 5 8 9 10 ovmpo ${⊢}\left({A}\in ℂ\wedge {T}\in \left({ℂ}^{ℋ}\right)\right)\to {A}{·}_{\mathrm{fn}}{T}=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)$
12 3 11 sylan2br ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℂ\right)\to {A}{·}_{\mathrm{fn}}{T}=\left({x}\in ℋ⟼{A}{T}\left({x}\right)\right)$