Metamath Proof Explorer

Theorem coesub

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

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

Proof

Step Hyp Ref Expression
1 coesub.1 
 |-  A = ( coeff ` F )
2 coesub.2 
 |-  B = ( coeff ` G )
3 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
4 simpl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
5 3 4 sseldi 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F e. ( Poly ` CC ) )
6 ssid 
 |-  CC C_ CC
7 neg1cn 
 |-  -u 1 e. CC
8 plyconst 
 |-  ( ( CC C_ CC /\ -u 1 e. CC ) -> ( CC X. { -u 1 } ) e. ( Poly ` CC ) )
9 6 7 8 mp2an 
 |-  ( CC X. { -u 1 } ) e. ( Poly ` CC )
10 simpr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
11 3 10 sseldi 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G e. ( Poly ` CC ) )
12 plymulcl 
 |-  ( ( ( CC X. { -u 1 } ) e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) ) -> ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` CC ) )
13 9 11 12 sylancr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` CC ) )
14 eqid 
 |-  ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) )
15 1 14 coeadd 
 |-  ( ( F e. ( Poly ` CC ) /\ ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` CC ) ) -> ( coeff ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) = ( A oF + ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) ) )
16 5 13 15 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) = ( A oF + ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) ) )
17 coemulc 
 |-  ( ( -u 1 e. CC /\ G e. ( Poly ` CC ) ) -> ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( ( NN0 X. { -u 1 } ) oF x. ( coeff ` G ) ) )
18 7 11 17 sylancr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( ( NN0 X. { -u 1 } ) oF x. ( coeff ` G ) ) )
19 2 oveq2i 
 |-  ( ( NN0 X. { -u 1 } ) oF x. B ) = ( ( NN0 X. { -u 1 } ) oF x. ( coeff ` G ) )
20 18 19 eqtr4di 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) = ( ( NN0 X. { -u 1 } ) oF x. B ) )
21 20 oveq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( A oF + ( coeff ` ( ( CC X. { -u 1 } ) oF x. G ) ) ) = ( A oF + ( ( NN0 X. { -u 1 } ) oF x. B ) ) )
22 16 21 eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) = ( A oF + ( ( NN0 X. { -u 1 } ) oF x. B ) ) )
23 cnex 
 |-  CC e. _V
24 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
25 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
26 ofnegsub 
 |-  ( ( CC e. _V /\ F : CC --> CC /\ G : CC --> CC ) -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
27 23 24 25 26 mp3an3an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
28 27 fveq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) ) = ( coeff ` ( F oF - G ) ) )
29 nn0ex 
 |-  NN0 e. _V
30 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
31 2 coef3 
 |-  ( G e. ( Poly ` S ) -> B : NN0 --> CC )
32 ofnegsub 
 |-  ( ( NN0 e. _V /\ A : NN0 --> CC /\ B : NN0 --> CC ) -> ( A oF + ( ( NN0 X. { -u 1 } ) oF x. B ) ) = ( A oF - B ) )
33 29 30 31 32 mp3an3an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( A oF + ( ( NN0 X. { -u 1 } ) oF x. B ) ) = ( A oF - B ) )
34 22 28 33 3eqtr3d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF - G ) ) = ( A oF - B ) )