Metamath Proof Explorer

Theorem pwsvscafval

Description: Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsvscaval.y 
|- Y = ( R ^s I )
pwsvscaval.b 
|- B = ( Base ` Y )
pwsvscaval.s 
|- .x. = ( .s ` R )
pwsvscaval.t 
|- .xb = ( .s ` Y )
pwsvscaval.f 
|- F = ( Scalar ` R )
pwsvscaval.k 
|- K = ( Base ` F )
pwsvscaval.r 
|- ( ph -> R e. V )
pwsvscaval.i 
|- ( ph -> I e. W )
pwsvscaval.a 
|- ( ph -> A e. K )
pwsvscaval.x 
|- ( ph -> X e. B )
Assertion pwsvscafval 
|- ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )

Proof

Step Hyp Ref Expression
1 pwsvscaval.y 
 |-  Y = ( R ^s I )
2 pwsvscaval.b 
 |-  B = ( Base ` Y )
3 pwsvscaval.s 
 |-  .x. = ( .s ` R )
4 pwsvscaval.t 
 |-  .xb = ( .s ` Y )
5 pwsvscaval.f 
 |-  F = ( Scalar ` R )
6 pwsvscaval.k 
 |-  K = ( Base ` F )
7 pwsvscaval.r 
 |-  ( ph -> R e. V )
8 pwsvscaval.i 
 |-  ( ph -> I e. W )
9 pwsvscaval.a 
 |-  ( ph -> A e. K )
10 pwsvscaval.x 
 |-  ( ph -> X e. B )
11 1 5 pwsval 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( F Xs_ ( I X. { R } ) ) )
12 7 8 11 syl2anc 
 |-  ( ph -> Y = ( F Xs_ ( I X. { R } ) ) )
13 12 fveq2d 
 |-  ( ph -> ( .s ` Y ) = ( .s ` ( F Xs_ ( I X. { R } ) ) ) )
14 4 13 syl5eq 
 |-  ( ph -> .xb = ( .s ` ( F Xs_ ( I X. { R } ) ) ) )
15 14 oveqd 
 |-  ( ph -> ( A .xb X ) = ( A ( .s ` ( F Xs_ ( I X. { R } ) ) ) X ) )
16 eqid 
 |-  ( F Xs_ ( I X. { R } ) ) = ( F Xs_ ( I X. { R } ) )
17 eqid 
 |-  ( Base ` ( F Xs_ ( I X. { R } ) ) ) = ( Base ` ( F Xs_ ( I X. { R } ) ) )
18 eqid 
 |-  ( .s ` ( F Xs_ ( I X. { R } ) ) ) = ( .s ` ( F Xs_ ( I X. { R } ) ) )
19 5 fvexi 
 |-  F e. _V
20 19 a1i 
 |-  ( ph -> F e. _V )
21 fnconstg 
 |-  ( R e. V -> ( I X. { R } ) Fn I )
22 7 21 syl 
 |-  ( ph -> ( I X. { R } ) Fn I )
23 12 fveq2d 
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( F Xs_ ( I X. { R } ) ) ) )
24 2 23 syl5eq 
 |-  ( ph -> B = ( Base ` ( F Xs_ ( I X. { R } ) ) ) )
25 10 24 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( F Xs_ ( I X. { R } ) ) ) )
26 16 17 18 6 20 8 22 9 25 prdsvscaval 
 |-  ( ph -> ( A ( .s ` ( F Xs_ ( I X. { R } ) ) ) X ) = ( x e. I |-> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) ) )
27 fvconst2g 
 |-  ( ( R e. V /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
28 7 27 sylan 
 |-  ( ( ph /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
29 28 fveq2d 
 |-  ( ( ph /\ x e. I ) -> ( .s ` ( ( I X. { R } ) ` x ) ) = ( .s ` R ) )
30 29 3 eqtr4di 
 |-  ( ( ph /\ x e. I ) -> ( .s ` ( ( I X. { R } ) ` x ) ) = .x. )
31 30 oveqd 
 |-  ( ( ph /\ x e. I ) -> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) = ( A .x. ( X ` x ) ) )
32 31 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) ) = ( x e. I |-> ( A .x. ( X ` x ) ) ) )
33 9 adantr 
 |-  ( ( ph /\ x e. I ) -> A e. K )
34 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( X ` x ) e. _V )
35 fconstmpt 
 |-  ( I X. { A } ) = ( x e. I |-> A )
36 35 a1i 
 |-  ( ph -> ( I X. { A } ) = ( x e. I |-> A ) )
37 eqid 
 |-  ( Base ` R ) = ( Base ` R )
38 1 37 2 7 8 10 pwselbas 
 |-  ( ph -> X : I --> ( Base ` R ) )
39 38 feqmptd 
 |-  ( ph -> X = ( x e. I |-> ( X ` x ) ) )
40 8 33 34 36 39 offval2 
 |-  ( ph -> ( ( I X. { A } ) oF .x. X ) = ( x e. I |-> ( A .x. ( X ` x ) ) ) )
41 32 40 eqtr4d 
 |-  ( ph -> ( x e. I |-> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) ) = ( ( I X. { A } ) oF .x. X ) )
42 15 26 41 3eqtrd 
 |-  ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )