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

Metamath Proof Explorer

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