Metamath Proof Explorer

Theorem mulvfv

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

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

Proof

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