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({ℂ}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼fg\left(x\right)\right)\right)$$

Detailed syntax breakdown

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