Theorem hfsmval

Description: Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hfsmval	|- ( ( S : ~H --> CC /\ T : ~H --> CC ) -> ( S +fn T ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnex	|- CC e. _V
2		ax-hilex	|- ~H e. _V
3	1 2	elmap	|- ( S e. ( CC ^m ~H ) <-> S : ~H --> CC )
4	1 2	elmap	|- ( T e. ( CC ^m ~H ) <-> T : ~H --> CC )
5		fveq1	|- ( f = S -> ( f ` x ) = ( S ` x ) )
6	5	oveq1d	|- ( f = S -> ( ( f ` x ) + ( g ` x ) ) = ( ( S ` x ) + ( g ` x ) ) )
7	6	mpteq2dv	|- ( f = S -> ( x e. ~H |-> ( ( f ` x ) + ( g ` x ) ) ) = ( x e. ~H |-> ( ( S ` x ) + ( g ` x ) ) ) )
8		fveq1	|- ( g = T -> ( g ` x ) = ( T ` x ) )
9	8	oveq2d	|- ( g = T -> ( ( S ` x ) + ( g ` x ) ) = ( ( S ` x ) + ( T ` x ) ) )
10	9	mpteq2dv	|- ( g = T -> ( x e. ~H |-> ( ( S ` x ) + ( g ` x ) ) ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) )
11		df-hfsum	|- +fn = ( f e. ( CC ^m ~H ) , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) + ( g ` x ) ) ) )
12	2	mptex	|- ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) e. _V
13	7 10 11 12	ovmpo	|- ( ( S e. ( CC ^m ~H ) /\ T e. ( CC ^m ~H ) ) -> ( S +fn T ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) )
14	3 4 13	syl2anbr	|- ( ( S : ~H --> CC /\ T : ~H --> CC ) -> ( S +fn T ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) )