Metamath Proof Explorer

Theorem addrval

Description: Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. C -> A e. _V )
2 elex 
 |-  ( B e. D -> B e. _V )
3 fveq1 
 |-  ( x = A -> ( x ` v ) = ( A ` v ) )
4 fveq1 
 |-  ( y = B -> ( y ` v ) = ( B ` v ) )
5 3 4 oveqan12d 
 |-  ( ( x = A /\ y = B ) -> ( ( x ` v ) + ( y ` v ) ) = ( ( A ` v ) + ( B ` v ) ) )
6 5 mpteq2dv 
 |-  ( ( x = A /\ y = B ) -> ( v e. RR |-> ( ( x ` v ) + ( y ` v ) ) ) = ( v e. RR |-> ( ( A ` v ) + ( B ` v ) ) ) )
7 df-addr 
 |-  +r = ( x e. _V , y e. _V |-> ( v e. RR |-> ( ( x ` v ) + ( y ` v ) ) ) )
8 reex 
 |-  RR e. _V
9 8 mptex 
 |-  ( v e. RR |-> ( ( A ` v ) + ( B ` v ) ) ) e. _V
10 6 7 9 ovmpoa 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A +r B ) = ( v e. RR |-> ( ( A ` v ) + ( B ` v ) ) ) )
11 1 2 10 syl2an 
 |-  ( ( A e. C /\ B e. D ) -> ( A +r B ) = ( v e. RR |-> ( ( A ` v ) + ( B ` v ) ) ) )