Metamath Proof Explorer

Theorem mulvval

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

Ref Expression
Assertion mulvval 
|- ( ( A e. C /\ B e. D ) -> ( A .v B ) = ( v e. RR |-> ( A x. ( 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 
 |-  ( y = B -> ( y ` v ) = ( B ` v ) )
4 oveq12 
 |-  ( ( x = A /\ ( y ` v ) = ( B ` v ) ) -> ( x x. ( y ` v ) ) = ( A x. ( B ` v ) ) )
5 3 4 sylan2 
 |-  ( ( x = A /\ y = B ) -> ( x x. ( y ` v ) ) = ( A x. ( B ` v ) ) )
6 5 mpteq2dv 
 |-  ( ( x = A /\ y = B ) -> ( v e. RR |-> ( x x. ( y ` v ) ) ) = ( v e. RR |-> ( A x. ( B ` v ) ) ) )
7 df-mulv 
 |-  .v = ( x e. _V , y e. _V |-> ( v e. RR |-> ( x x. ( y ` v ) ) ) )
8 reex 
 |-  RR e. _V
9 8 mptex 
 |-  ( v e. RR |-> ( A x. ( B ` v ) ) ) e. _V
10 6 7 9 ovmpoa 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A .v B ) = ( v e. RR |-> ( A x. ( B ` v ) ) ) )
11 1 2 10 syl2an 
 |-  ( ( A e. C /\ B e. D ) -> ( A .v B ) = ( v e. RR |-> ( A x. ( B ` v ) ) ) )