Definition df-hfsum

Description: Define the sum of two Hilbert space functionals. Definition of Beran p. 111. Note that unlike some authors, we define a functional as any function from ~H to CC , not just linear (or bounded linear) ones. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hfsum	|- +fn = ( f e. ( CC ^m ~H ) , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) + ( g ` x ) ) ) )

Detailed syntax breakdown

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