Metamath Proof Explorer

Theorem hfsval

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

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

Proof

Step Hyp Ref Expression
1 hfsmval 
 |-  ( ( S : ~H --> CC /\ T : ~H --> CC ) -> ( S +fn T ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) )
2 1 fveq1d 
 |-  ( ( S : ~H --> CC /\ T : ~H --> CC ) -> ( ( S +fn T ) ` A ) = ( ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) ` A ) )
3 fveq2 
 |-  ( x = A -> ( S ` x ) = ( S ` A ) )
4 fveq2 
 |-  ( x = A -> ( T ` x ) = ( T ` A ) )
5 3 4 oveq12d 
 |-  ( x = A -> ( ( S ` x ) + ( T ` x ) ) = ( ( S ` A ) + ( T ` A ) ) )
6 eqid 
 |-  ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) )
7 ovex 
 |-  ( ( S ` A ) + ( T ` A ) ) e. _V
8 5 6 7 fvmpt 
 |-  ( A e. ~H -> ( ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) ` A ) = ( ( S ` A ) + ( T ` A ) ) )
9 2 8 sylan9eq 
 |-  ( ( ( S : ~H --> CC /\ T : ~H --> CC ) /\ A e. ~H ) -> ( ( S +fn T ) ` A ) = ( ( S ` A ) + ( T ` A ) ) )
10 9 3impa 
 |-  ( ( S : ~H --> CC /\ T : ~H --> CC /\ A e. ~H ) -> ( ( S +fn T ) ` A ) = ( ( S ` A ) + ( T ` A ) ) )