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 : T : A S + fn T A = S A + T A

Proof

Step Hyp Ref Expression
1 hfsmval S : T : S + fn T = x S x + T x
2 1 fveq1d S : T : S + fn T A = x 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 S x + T x = x S x + T x
7 ovex S A + T A V
8 5 6 7 fvmpt A x S x + T x A = S A + T A
9 2 8 sylan9eq S : T : A S + fn T A = S A + T A
10 9 3impa S : T : A S + fn T A = S A + T A