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	2	fvexi	|- B e. _V
11	1 8 2	mplval2	|- P = ( ( I mPwSer R ) |`s B )
12		eqid	|- ( .r ` ( I mPwSer R ) ) = ( .r ` ( I mPwSer R ) )
13	11 12	ressmulr	|- ( B e. _V -> ( .r ` ( I mPwSer R ) ) = ( .r ` P ) )
14	10 13	ax-mp	|- ( .r ` ( I mPwSer R ) ) = ( .r ` P )
15	4 14	eqtr4i	|- .xb = ( .r ` ( I mPwSer R ) )
16	1 8 2 9	mplbasss	|- B C_ ( Base ` ( I mPwSer R ) )
17	16 6	sseldi	|- ( ph -> F e. ( Base ` ( I mPwSer R ) ) )
18	16 7	sseldi	|- ( ph -> G e. ( Base ` ( I mPwSer R ) ) )
19	8 9 3 15 5 17 18	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 ) ) ) ) ) ) )