This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrmulval

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 )
psrmulval.r 
|- ( ph -> X e. D )
Assertion psrmulval 
|- ( ph -> ( ( F .xb G ) ` X ) = ( R gsum ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )

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 psrmulval.r 
 |-  ( ph -> X e. D )
9 1 2 3 4 5 6 7 psrmulfval 
 |-  ( ph -> ( F .xb G ) = ( x e. D |-> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) ) )
10 9 fveq1d 
 |-  ( ph -> ( ( F .xb G ) ` X ) = ( ( x e. D |-> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) ) ` X ) )
11 breq2 
 |-  ( x = X -> ( y oR <_ x <-> y oR <_ X ) )
12 11 rabbidv 
 |-  ( x = X -> { y e. D | y oR <_ x } = { y e. D | y oR <_ X } )
13 fvoveq1 
 |-  ( x = X -> ( G ` ( x oF - k ) ) = ( G ` ( X oF - k ) ) )
14 13 oveq2d 
 |-  ( x = X -> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) = ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) )
15 12 14 mpteq12dv 
 |-  ( x = X -> ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) = ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) )
16 15 oveq2d 
 |-  ( x = X -> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) = ( R gsum ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )
17 eqid 
 |-  ( x e. D |-> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) ) = ( x e. D |-> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) )
18 ovex 
 |-  ( R gsum ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) e. _V
19 16 17 18 fvmpt 
 |-  ( X e. D -> ( ( x e. D |-> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) ) ` X ) = ( R gsum ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )
20 8 19 syl 
 |-  ( ph -> ( ( x e. D |-> ( R gsum ( k e. { y e. D | y oR <_ x } |-> ( ( F ` k ) .x. ( G ` ( x oF - k ) ) ) ) ) ) ` X ) = ( R gsum ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )
21 10 20 eqtrd 
 |-  ( ph -> ( ( F .xb G ) ` X ) = ( R gsum ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )