Metamath Proof Explorer


Theorem prdsvscaval

Description: Scalar multiplication in a structure product is pointwise. (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 )
Assertion prdsvscaval
|- ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )

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 fnex
 |-  ( ( R Fn I /\ I e. W ) -> R e. _V )
11 7 6 10 syl2anc
 |-  ( ph -> R e. _V )
12 7 fndmd
 |-  ( ph -> dom R = I )
13 1 5 11 2 12 4 3 prdsvsca
 |-  ( ph -> .x. = ( y e. K , z e. B |-> ( x e. I |-> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) ) ) )
14 id
 |-  ( y = F -> y = F )
15 fveq1
 |-  ( z = G -> ( z ` x ) = ( G ` x ) )
16 14 15 oveqan12d
 |-  ( ( y = F /\ z = G ) -> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) = ( F ( .s ` ( R ` x ) ) ( G ` x ) ) )
17 16 adantl
 |-  ( ( ph /\ ( y = F /\ z = G ) ) -> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) = ( F ( .s ` ( R ` x ) ) ( G ` x ) ) )
18 17 mpteq2dv
 |-  ( ( ph /\ ( y = F /\ z = G ) ) -> ( x e. I |-> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )
19 6 mptexd
 |-  ( ph -> ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) e. _V )
20 13 18 8 9 19 ovmpod
 |-  ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )