Metamath Proof Explorer

Theorem pwsmulrval

Description: Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsplusgval.y 
|- Y = ( R ^s I )
pwsplusgval.b 
|- B = ( Base ` Y )
pwsplusgval.r 
|- ( ph -> R e. V )
pwsplusgval.i 
|- ( ph -> I e. W )
pwsplusgval.f 
|- ( ph -> F e. B )
pwsplusgval.g 
|- ( ph -> G e. B )
pwsmulrval.a 
|- .x. = ( .r ` R )
pwsmulrval.p 
|- .xb = ( .r ` Y )
Assertion pwsmulrval 
|- ( ph -> ( F .xb G ) = ( F oF .x. G ) )

Proof

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