Metamath Proof Explorer

Theorem coe1mul

Description: The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul.s 
|- Y = ( Poly1 ` R )
coe1mul.t 
|- .xb = ( .r ` Y )
coe1mul.u 
|- .x. = ( .r ` R )
coe1mul.b 
|- B = ( Base ` Y )
Assertion coe1mul 
|- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 coe1mul.s 
 |-  Y = ( Poly1 ` R )
2 coe1mul.t 
 |-  .xb = ( .r ` Y )
3 coe1mul.u 
 |-  .x. = ( .r ` R )
4 coe1mul.b 
 |-  B = ( Base ` Y )
5 id 
 |-  ( R e. Ring -> R e. Ring )
6 1 4 ply1bascl 
 |-  ( F e. B -> F e. ( Base ` ( PwSer1 ` R ) ) )
7 1 4 ply1bascl 
 |-  ( G e. B -> G e. ( Base ` ( PwSer1 ` R ) ) )
8 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
9 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
10 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
11 1 9 2 ply1mulr 
 |-  .xb = ( .r ` ( 1o mPoly R ) )
12 9 10 11 mplmulr 
 |-  .xb = ( .r ` ( 1o mPwSer R ) )
13 eqid 
 |-  ( .r ` ( PwSer1 ` R ) ) = ( .r ` ( PwSer1 ` R ) )
14 8 10 13 psr1mulr 
 |-  ( .r ` ( PwSer1 ` R ) ) = ( .r ` ( 1o mPwSer R ) )
15 12 14 eqtr4i 
 |-  .xb = ( .r ` ( PwSer1 ` R ) )
16 eqid 
 |-  ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( PwSer1 ` R ) )
17 8 15 3 16 coe1mul2 
 |-  ( ( R e. Ring /\ F e. ( Base ` ( PwSer1 ` R ) ) /\ G e. ( Base ` ( PwSer1 ` R ) ) ) -> ( coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) ) )
18 5 6 7 17 syl3an 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) ) )