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

Metamath Proof Explorer

Theorem coemul

Description: A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 
|- A = ( coeff ` F )
coeadd.2 
|- B = ( coeff ` G )
Assertion coemul 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( coeff ` ( F oF x. G ) ) ` N ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 
 |-  A = ( coeff ` F )
2 coeadd.2 
 |-  B = ( coeff ` G )
3 eqid 
 |-  ( deg ` F ) = ( deg ` F )
4 eqid 
 |-  ( deg ` G ) = ( deg ` G )
5 1 2 3 4 coemullem 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) /\ ( deg ` ( F oF x. G ) ) <_ ( ( deg ` F ) + ( deg ` G ) ) ) )
6 5 simpld 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) )
7 6 fveq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) ` N ) = ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` N ) )
8 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
9 fvoveq1 
 |-  ( n = N -> ( B ` ( n - k ) ) = ( B ` ( N - k ) ) )
10 9 oveq2d 
 |-  ( n = N -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) = ( ( A ` k ) x. ( B ` ( N - k ) ) ) )
11 10 adantr 
 |-  ( ( n = N /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) = ( ( A ` k ) x. ( B ` ( N - k ) ) ) )
12 8 11 sumeq12dv 
 |-  ( n = N -> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) )
13 eqid 
 |-  ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) )
14 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) e. _V
15 12 13 14 fvmpt 
 |-  ( N e. NN0 -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` N ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) )
16 7 15 sylan9eq 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ N e. NN0 ) -> ( ( coeff ` ( F oF x. G ) ) ` N ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) )
17 16 3impa 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( coeff ` ( F oF x. G ) ) ` N ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( B ` ( N - k ) ) ) )