Theorem addrfv

Description: Vector addition at a value. The operation takes each vector A and B and forms a new vector whose values are the sum of each of the values of A and B . (Contributed by Andrew Salmon, 27-Jan-2012)

	Ref	Expression
Assertion	addrfv	|- ( ( A e. E /\ B e. D /\ C e. RR ) -> ( ( A +r B ) ` C ) = ( ( A ` C ) + ( B ` C ) ) )

Proof

Step	Hyp	Ref	Expression
1		addrval	|- ( ( A e. E /\ B e. D ) -> ( A +r B ) = ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) )
2	1	fveq1d	|- ( ( A e. E /\ B e. D ) -> ( ( A +r B ) ` C ) = ( ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) ` C ) )
3		fveq2	|- ( x = C -> ( A ` x ) = ( A ` C ) )
4		fveq2	|- ( x = C -> ( B ` x ) = ( B ` C ) )
5	3 4	oveq12d	|- ( x = C -> ( ( A ` x ) + ( B ` x ) ) = ( ( A ` C ) + ( B ` C ) ) )
6		eqid	|- ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) = ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) )
7		ovex	|- ( ( A ` C ) + ( B ` C ) ) e. _V
8	5 6 7	fvmpt	|- ( C e. RR -> ( ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) ` C ) = ( ( A ` C ) + ( B ` C ) ) )
9	2 8	sylan9eq	|- ( ( ( A e. E /\ B e. D ) /\ C e. RR ) -> ( ( A +r B ) ` C ) = ( ( A ` C ) + ( B ` C ) ) )
10	9	3impa	|- ( ( A e. E /\ B e. D /\ C e. RR ) -> ( ( A +r B ) ` C ) = ( ( A ` C ) + ( B ` C ) ) )