Metamath Proof Explorer

Theorem coeadd

Description: The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 
|- A = ( coeff ` F )
coeadd.2 
|- B = ( coeff ` G )
Assertion coeadd 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + G ) ) = ( A oF + B ) )

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 coeaddlem 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF + G ) ) = ( A oF + B ) /\ ( deg ` ( F oF + G ) ) <_ if ( ( deg ` F ) <_ ( deg ` G ) , ( deg ` G ) , ( deg ` F ) ) ) )
6 5 simpld 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + G ) ) = ( A oF + B ) )