Theorem mplmul

Description: The multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mplmul.p	|- P = ( I mPoly R )
	mplmul.b	|- B = ( Base ` P )
	mplmul.m	|- .x. = ( .r ` R )
	mplmul.t	|- .xb = ( .r ` P )
	mplmul.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	mplmul.f	|- ( ph -> F e. B )
	mplmul.g	|- ( ph -> G e. B )
Assertion	mplmul	|- ( 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		mplmul.p	|- P = ( I mPoly R )
2		mplmul.b	|- B = ( Base ` P )
3		mplmul.m	|- .x. = ( .r ` R )
4		mplmul.t	|- .xb = ( .r ` P )
5		mplmul.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6		mplmul.f	|- ( ph -> F e. B )
7		mplmul.g	|- ( ph -> G e. B )
8		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
9		eqid	|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
10	1 8 4	mplmulr	|- .xb = ( .r ` ( I mPwSer R ) )
11	1 8 2 9	mplbasss	|- B C_ ( Base ` ( I mPwSer R ) )
12	11 6	sselid	|- ( ph -> F e. ( Base ` ( I mPwSer R ) ) )
13	11 7	sselid	|- ( ph -> G e. ( Base ` ( I mPwSer R ) ) )
14	8 9 3 10 5 12 13	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 ) ) ) ) ) ) )