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 eqtrid
 |-  ( 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 eqtrid
 |-  ( 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 ) )