This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsvscafval

Description: Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsbasmpt.y 
|- Y = ( S Xs_ R )
prdsbasmpt.b 
|- B = ( Base ` Y )
prdsvscaval.t 
|- .x. = ( .s ` Y )
prdsvscaval.k 
|- K = ( Base ` S )
prdsvscaval.s 
|- ( ph -> S e. V )
prdsvscaval.i 
|- ( ph -> I e. W )
prdsvscaval.r 
|- ( ph -> R Fn I )
prdsvscaval.f 
|- ( ph -> F e. K )
prdsvscaval.g 
|- ( ph -> G e. B )
prdsvscafval.j 
|- ( ph -> J e. I )
Assertion prdsvscafval 
|- ( ph -> ( ( F .x. G ) ` J ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y 
 |-  Y = ( S Xs_ R )
2 prdsbasmpt.b 
 |-  B = ( Base ` Y )
3 prdsvscaval.t 
 |-  .x. = ( .s ` Y )
4 prdsvscaval.k 
 |-  K = ( Base ` S )
5 prdsvscaval.s 
 |-  ( ph -> S e. V )
6 prdsvscaval.i 
 |-  ( ph -> I e. W )
7 prdsvscaval.r 
 |-  ( ph -> R Fn I )
8 prdsvscaval.f 
 |-  ( ph -> F e. K )
9 prdsvscaval.g 
 |-  ( ph -> G e. B )
10 prdsvscafval.j 
 |-  ( ph -> J e. I )
11 1 2 3 4 5 6 7 8 9 prdsvscaval 
 |-  ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )
12 2fveq3 
 |-  ( x = J -> ( .s ` ( R ` x ) ) = ( .s ` ( R ` J ) ) )
13 eqidd 
 |-  ( x = J -> F = F )
14 fveq2 
 |-  ( x = J -> ( G ` x ) = ( G ` J ) )
15 12 13 14 oveq123d 
 |-  ( x = J -> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )
16 15 adantl 
 |-  ( ( ph /\ x = J ) -> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )
17 ovexd 
 |-  ( ph -> ( F ( .s ` ( R ` J ) ) ( G ` J ) ) e. _V )
18 11 16 10 17 fvmptd 
 |-  ( ph -> ( ( F .x. G ) ` J ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )