Metamath Proof Explorer

Theorem psrmulfval

Description: The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrmulr.s 
|- S = ( I mPwSer R )
psrmulr.b 
|- B = ( Base ` S )
psrmulr.m 
|- .x. = ( .r ` R )
psrmulr.t 
|- .xb = ( .r ` S )
psrmulr.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
psrmulfval.i 
|- ( ph -> F e. B )
psrmulfval.r 
|- ( ph -> G e. B )
Assertion psrmulfval 
|- ( ph -> ( F .xb G ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrmulr.s 
 |-  S = ( I mPwSer R )
2 psrmulr.b 
 |-  B = ( Base ` S )
3 psrmulr.m 
 |-  .x. = ( .r ` R )
4 psrmulr.t 
 |-  .xb = ( .r ` S )
5 psrmulr.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 psrmulfval.i 
 |-  ( ph -> F e. B )
7 psrmulfval.r 
 |-  ( ph -> G e. B )
8 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
9 fveq1 
 |-  ( g = G -> ( g ` ( k oF - x ) ) = ( G ` ( k oF - x ) ) )
10 8 9 oveqan12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) = ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) )
11 10 mpteq2dv 
 |-  ( ( f = F /\ g = G ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) )
12 11 oveq2d 
 |-  ( ( f = F /\ g = G ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) = ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) )
13 12 mpteq2dv 
 |-  ( ( f = F /\ g = G ) -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) ) )
14 1 2 3 4 5 psrmulr 
 |-  .xb = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
15 ovex 
 |-  ( NN0 ^m I ) e. _V
16 5 15 rabex2 
 |-  D e. _V
17 16 mptex 
 |-  ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) ) e. _V
18 13 14 17 ovmpoa 
 |-  ( ( F e. B /\ G e. B ) -> ( F .xb G ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) ) )
19 6 7 18 syl2anc 
 |-  ( ph -> ( F .xb G ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) ) )