# Metamath Proof Explorer

## Definition df-hfmul

Description: Define the scalar product with a Hilbert space functional. Definition of Beran p. 111. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion df-hfmul ${⊢}{·}_{\mathrm{fn}}=\left({f}\in ℂ,{g}\in \left({ℂ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}{g}\left({x}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chft ${class}{·}_{\mathrm{fn}}$
1 vf ${setvar}{f}$
2 cc ${class}ℂ$
3 vg ${setvar}{g}$
4 cmap ${class}{↑}_{𝑚}$
5 chba ${class}ℋ$
6 2 5 4 co ${class}\left({ℂ}^{ℋ}\right)$
7 vx ${setvar}{x}$
8 1 cv ${setvar}{f}$
9 cmul ${class}×$
10 3 cv ${setvar}{g}$
11 7 cv ${setvar}{x}$
12 11 10 cfv ${class}{g}\left({x}\right)$
13 8 12 9 co ${class}{f}{g}\left({x}\right)$
14 7 5 13 cmpt ${class}\left({x}\in ℋ⟼{f}{g}\left({x}\right)\right)$
15 1 3 2 6 14 cmpo ${class}\left({f}\in ℂ,{g}\in \left({ℂ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}{g}\left({x}\right)\right)\right)$
16 0 15 wceq ${wff}{·}_{\mathrm{fn}}=\left({f}\in ℂ,{g}\in \left({ℂ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}{g}\left({x}\right)\right)\right)$