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	|- .fn = ( f e. CC , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( f x. ( g ` x ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chft	|- .fn
1		vf	|- f
2		cc	|- CC
3		vg	|- g
4		cmap	|- ^m
5		chba	|- ~H
6	2 5 4	co	|- ( CC ^m ~H )
7		vx	|- x
8	1	cv	|- f
9		cmul	|- x.
10	3	cv	|- g
11	7	cv	|- x
12	11 10	cfv	|- ( g ` x )
13	8 12 9	co	|- ( f x. ( g ` x ) )
14	7 5 13	cmpt	|- ( x e. ~H |-> ( f x. ( g ` x ) ) )
15	1 3 2 6 14	cmpo	|- ( f e. CC , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( f x. ( g ` x ) ) ) )
16	0 15	wceq	|- .fn = ( f e. CC , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( f x. ( g ` x ) ) ) )