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