Metamath Proof Explorer

Theorem subrfv

Description: Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 subrval 
 |-  ( ( 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 ) ) )