Metamath Proof Explorer

Theorem plymulx

Description: Coefficients of a polynomial multiplied by Xp . (Contributed by Thierry Arnoux, 25-Sep-2018)

Ref Expression
Assertion plymulx 
|- ( F e. ( Poly ` RR ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-resscn 
 |-  RR C_ CC
2 1re 
 |-  1 e. RR
3 plyid 
 |-  ( ( RR C_ CC /\ 1 e. RR ) -> Xp e. ( Poly ` RR ) )
4 1 2 3 mp2an 
 |-  Xp e. ( Poly ` RR )
5 plymul02 
 |-  ( Xp e. ( Poly ` RR ) -> ( 0p oF x. Xp ) = 0p )
6 5 fveq2d 
 |-  ( Xp e. ( Poly ` RR ) -> ( coeff ` ( 0p oF x. Xp ) ) = ( coeff ` 0p ) )
7 4 6 ax-mp 
 |-  ( coeff ` ( 0p oF x. Xp ) ) = ( coeff ` 0p )
8 fconstmpt 
 |-  ( NN0 X. { 0 } ) = ( n e. NN0 |-> 0 )
9 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
10 eqidd 
 |-  ( ( n e. NN0 /\ n = 0 ) -> 0 = 0 )
11 elnnne0 
 |-  ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
12 df-ne 
 |-  ( n =/= 0 <-> -. n = 0 )
13 12 anbi2i 
 |-  ( ( n e. NN0 /\ n =/= 0 ) <-> ( n e. NN0 /\ -. n = 0 ) )
14 11 13 bitr2i 
 |-  ( ( n e. NN0 /\ -. n = 0 ) <-> n e. NN )
15 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
16 14 15 sylbi 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> ( n - 1 ) e. NN0 )
17 eqidd 
 |-  ( m = ( n - 1 ) -> 0 = 0 )
18 fconstmpt 
 |-  ( NN0 X. { 0 } ) = ( m e. NN0 |-> 0 )
19 9 18 eqtri 
 |-  ( coeff ` 0p ) = ( m e. NN0 |-> 0 )
20 c0ex 
 |-  0 e. _V
21 17 19 20 fvmpt 
 |-  ( ( n - 1 ) e. NN0 -> ( ( coeff ` 0p ) ` ( n - 1 ) ) = 0 )
22 16 21 syl 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> ( ( coeff ` 0p ) ` ( n - 1 ) ) = 0 )
23 10 22 ifeqda 
 |-  ( n e. NN0 -> if ( n = 0 , 0 , ( ( coeff ` 0p ) ` ( n - 1 ) ) ) = 0 )
24 23 mpteq2ia 
 |-  ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` 0p ) ` ( n - 1 ) ) ) ) = ( n e. NN0 |-> 0 )
25 8 9 24 3eqtr4ri 
 |-  ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` 0p ) ` ( n - 1 ) ) ) ) = ( coeff ` 0p )
26 7 25 eqtr4i 
 |-  ( coeff ` ( 0p oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` 0p ) ` ( n - 1 ) ) ) )
27 fvoveq1 
 |-  ( F = 0p -> ( coeff ` ( F oF x. Xp ) ) = ( coeff ` ( 0p oF x. Xp ) ) )
28 simpl 
 |-  ( ( F = 0p /\ n e. NN0 ) -> F = 0p )
29 28 fveq2d 
 |-  ( ( F = 0p /\ n e. NN0 ) -> ( coeff ` F ) = ( coeff ` 0p ) )
30 29 fveq1d 
 |-  ( ( F = 0p /\ n e. NN0 ) -> ( ( coeff ` F ) ` ( n - 1 ) ) = ( ( coeff ` 0p ) ` ( n - 1 ) ) )
31 30 ifeq2d 
 |-  ( ( F = 0p /\ n e. NN0 ) -> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) = if ( n = 0 , 0 , ( ( coeff ` 0p ) ` ( n - 1 ) ) ) )
32 31 mpteq2dva 
 |-  ( F = 0p -> ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` 0p ) ` ( n - 1 ) ) ) ) )
33 26 27 32 3eqtr4a 
 |-  ( F = 0p -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
34 33 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ F = 0p ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
35 simpl 
 |-  ( ( F e. ( Poly ` RR ) /\ -. F = 0p ) -> F e. ( Poly ` RR ) )
36 elsng 
 |-  ( F e. ( Poly ` RR ) -> ( F e. { 0p } <-> F = 0p ) )
37 36 notbid 
 |-  ( F e. ( Poly ` RR ) -> ( -. F e. { 0p } <-> -. F = 0p ) )
38 37 biimpar 
 |-  ( ( F e. ( Poly ` RR ) /\ -. F = 0p ) -> -. F e. { 0p } )
39 35 38 eldifd 
 |-  ( ( F e. ( Poly ` RR ) /\ -. F = 0p ) -> F e. ( ( Poly ` RR ) \ { 0p } ) )
40 plymulx0 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
41 39 40 syl 
 |-  ( ( F e. ( Poly ` RR ) /\ -. F = 0p ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
42 34 41 pm2.61dan 
 |-  ( F e. ( Poly ` RR ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )