Metamath Proof Explorer

Theorem plymulx0

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

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

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> F e. ( Poly ` RR ) )
2 ax-resscn 
 |-  RR C_ CC
3 1re 
 |-  1 e. RR
4 plyid 
 |-  ( ( RR C_ CC /\ 1 e. RR ) -> Xp e. ( Poly ` RR ) )
5 2 3 4 mp2an 
 |-  Xp e. ( Poly ` RR )
6 5 a1i 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> Xp e. ( Poly ` RR ) )
7 simprl 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> x e. RR )
8 simprr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> y e. RR )
9 7 8 readdcld 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
10 7 8 remulcld 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
11 1 6 9 10 plymul 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( F oF x. Xp ) e. ( Poly ` RR ) )
12 0re 
 |-  0 e. RR
13 eqid 
 |-  ( coeff ` ( F oF x. Xp ) ) = ( coeff ` ( F oF x. Xp ) )
14 13 coef2 
 |-  ( ( ( F oF x. Xp ) e. ( Poly ` RR ) /\ 0 e. RR ) -> ( coeff ` ( F oF x. Xp ) ) : NN0 --> RR )
15 11 12 14 sylancl 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` ( F oF x. Xp ) ) : NN0 --> RR )
16 15 feqmptd 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> ( ( coeff ` ( F oF x. Xp ) ) ` n ) ) )
17 cnex 
 |-  CC e. _V
18 17 a1i 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> CC e. _V )
19 plyf 
 |-  ( F e. ( Poly ` RR ) -> F : CC --> CC )
20 1 19 syl 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> F : CC --> CC )
21 plyf 
 |-  ( Xp e. ( Poly ` RR ) -> Xp : CC --> CC )
22 5 21 ax-mp 
 |-  Xp : CC --> CC
23 22 a1i 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> Xp : CC --> CC )
24 simprl 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. CC /\ y e. CC ) ) -> x e. CC )
25 simprr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. CC /\ y e. CC ) ) -> y e. CC )
26 24 25 mulcomd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) = ( y x. x ) )
27 18 20 23 26 caofcom 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( F oF x. Xp ) = ( Xp oF x. F ) )
28 27 fveq2d 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` ( F oF x. Xp ) ) = ( coeff ` ( Xp oF x. F ) ) )
29 28 fveq1d 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( ( coeff ` ( F oF x. Xp ) ) ` n ) = ( ( coeff ` ( Xp oF x. F ) ) ` n ) )
30 29 adantr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( ( coeff ` ( F oF x. Xp ) ) ` n ) = ( ( coeff ` ( Xp oF x. F ) ) ` n ) )
31 5 a1i 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> Xp e. ( Poly ` RR ) )
32 1 adantr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> F e. ( Poly ` RR ) )
33 simpr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> n e. NN0 )
34 eqid 
 |-  ( coeff ` Xp ) = ( coeff ` Xp )
35 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
36 34 35 coemul 
 |-  ( ( Xp e. ( Poly ` RR ) /\ F e. ( Poly ` RR ) /\ n e. NN0 ) -> ( ( coeff ` ( Xp oF x. F ) ) ` n ) = sum_ i e. ( 0 ... n ) ( ( ( coeff ` Xp ) ` i ) x. ( ( coeff ` F ) ` ( n - i ) ) ) )
37 31 32 33 36 syl3anc 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( ( coeff ` ( Xp oF x. F ) ) ` n ) = sum_ i e. ( 0 ... n ) ( ( ( coeff ` Xp ) ` i ) x. ( ( coeff ` F ) ` ( n - i ) ) ) )
38 elfznn0 
 |-  ( i e. ( 0 ... n ) -> i e. NN0 )
39 coeidp 
 |-  ( i e. NN0 -> ( ( coeff ` Xp ) ` i ) = if ( i = 1 , 1 , 0 ) )
40 38 39 syl 
 |-  ( i e. ( 0 ... n ) -> ( ( coeff ` Xp ) ` i ) = if ( i = 1 , 1 , 0 ) )
41 40 oveq1d 
 |-  ( i e. ( 0 ... n ) -> ( ( ( coeff ` Xp ) ` i ) x. ( ( coeff ` F ) ` ( n - i ) ) ) = ( if ( i = 1 , 1 , 0 ) x. ( ( coeff ` F ) ` ( n - i ) ) ) )
42 ovif 
 |-  ( if ( i = 1 , 1 , 0 ) x. ( ( coeff ` F ) ` ( n - i ) ) ) = if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) )
43 41 42 eqtrdi 
 |-  ( i e. ( 0 ... n ) -> ( ( ( coeff ` Xp ) ` i ) x. ( ( coeff ` F ) ` ( n - i ) ) ) = if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) ) )
44 43 adantl 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( ( ( coeff ` Xp ) ` i ) x. ( ( coeff ` F ) ` ( n - i ) ) ) = if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) ) )
45 44 sumeq2dv 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) ( ( ( coeff ` Xp ) ` i ) x. ( ( coeff ` F ) ` ( n - i ) ) ) = sum_ i e. ( 0 ... n ) if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) ) )
46 velsn 
 |-  ( i e. { 1 } <-> i = 1 )
47 46 bicomi 
 |-  ( i = 1 <-> i e. { 1 } )
48 47 a1i 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( i = 1 <-> i e. { 1 } ) )
49 35 coef2 
 |-  ( ( F e. ( Poly ` RR ) /\ 0 e. RR ) -> ( coeff ` F ) : NN0 --> RR )
50 1 12 49 sylancl 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` F ) : NN0 --> RR )
51 50 ad2antrr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( coeff ` F ) : NN0 --> RR )
52 fznn0sub 
 |-  ( i e. ( 0 ... n ) -> ( n - i ) e. NN0 )
53 52 adantl 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( n - i ) e. NN0 )
54 51 53 ffvelcdmd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( ( coeff ` F ) ` ( n - i ) ) e. RR )
55 54 recnd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( ( coeff ` F ) ` ( n - i ) ) e. CC )
56 55 mullidd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) = ( ( coeff ` F ) ` ( n - i ) ) )
57 55 mul02d 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) = 0 )
58 48 56 57 ifbieq12d 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) ) = if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) )
59 58 sumeq2dv 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) ) = sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) )
60 eqeq2 
 |-  ( 0 = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) -> ( sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 <-> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
61 eqeq2 
 |-  ( ( ( coeff ` F ) ` ( n - 1 ) ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) -> ( sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = ( ( coeff ` F ) ` ( n - 1 ) ) <-> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
62 oveq2 
 |-  ( n = 0 -> ( 0 ... n ) = ( 0 ... 0 ) )
63 0z 
 |-  0 e. ZZ
64 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
65 63 64 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
66 62 65 eqtrdi 
 |-  ( n = 0 -> ( 0 ... n ) = { 0 } )
67 elsni 
 |-  ( i e. { 0 } -> i = 0 )
68 67 adantl 
 |-  ( ( n = 0 /\ i e. { 0 } ) -> i = 0 )
69 ax-1ne0 
 |-  1 =/= 0
70 69 nesymi 
 |-  -. 0 = 1
71 eqeq1 
 |-  ( i = 0 -> ( i = 1 <-> 0 = 1 ) )
72 70 71 mtbiri 
 |-  ( i = 0 -> -. i = 1 )
73 47 notbii 
 |-  ( -. i = 1 <-> -. i e. { 1 } )
74 73 biimpi 
 |-  ( -. i = 1 -> -. i e. { 1 } )
75 iffalse 
 |-  ( -. i e. { 1 } -> if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
76 68 72 74 75 4syl 
 |-  ( ( n = 0 /\ i e. { 0 } ) -> if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
77 66 76 sumeq12rdv 
 |-  ( n = 0 -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = sum_ i e. { 0 } 0 )
78 snfi 
 |-  { 0 } e. Fin
79 78 olci 
 |-  ( { 0 } C_ ( ZZ>= ` 0 ) \/ { 0 } e. Fin )
80 sumz 
 |-  ( ( { 0 } C_ ( ZZ>= ` 0 ) \/ { 0 } e. Fin ) -> sum_ i e. { 0 } 0 = 0 )
81 79 80 ax-mp 
 |-  sum_ i e. { 0 } 0 = 0
82 77 81 eqtrdi 
 |-  ( n = 0 -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
83 82 adantl 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ n = 0 ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
84 simpll 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> F e. ( ( Poly ` RR ) \ { 0p } ) )
85 33 adantr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN0 )
86 simpr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> -. n = 0 )
87 86 neqned 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n =/= 0 )
88 elnnne0 
 |-  ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
89 85 87 88 sylanbrc 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
90 1nn0 
 |-  1 e. NN0
91 90 a1i 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 e. NN0 )
92 simpr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> n e. NN )
93 92 nnnn0d 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> n e. NN0 )
94 92 nnge1d 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 <_ n )
95 elfz2nn0 
 |-  ( 1 e. ( 0 ... n ) <-> ( 1 e. NN0 /\ n e. NN0 /\ 1 <_ n ) )
96 91 93 94 95 syl3anbrc 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 e. ( 0 ... n ) )
97 96 snssd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> { 1 } C_ ( 0 ... n ) )
98 50 ad2antrr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( coeff ` F ) : NN0 --> RR )
99 oveq2 
 |-  ( i = 1 -> ( n - i ) = ( n - 1 ) )
100 46 99 sylbi 
 |-  ( i e. { 1 } -> ( n - i ) = ( n - 1 ) )
101 100 adantl 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - i ) = ( n - 1 ) )
102 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
103 102 ad2antlr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - 1 ) e. NN0 )
104 101 103 eqeltrd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - i ) e. NN0 )
105 98 104 ffvelcdmd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( ( coeff ` F ) ` ( n - i ) ) e. RR )
106 105 recnd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( ( coeff ` F ) ` ( n - i ) ) e. CC )
107 106 ralrimiva 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> A. i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) e. CC )
108 fzfi 
 |-  ( 0 ... n ) e. Fin
109 108 olci 
 |-  ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin )
110 109 a1i 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin ) )
111 sumss2 
 |-  ( ( ( { 1 } C_ ( 0 ... n ) /\ A. i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) e. CC ) /\ ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin ) ) -> sum_ i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) = sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) )
112 97 107 110 111 syl21anc 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) = sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) )
113 50 adantr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( coeff ` F ) : NN0 --> RR )
114 102 adantl 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( n - 1 ) e. NN0 )
115 113 114 ffvelcdmd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( coeff ` F ) ` ( n - 1 ) ) e. RR )
116 115 recnd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( coeff ` F ) ` ( n - 1 ) ) e. CC )
117 99 fveq2d 
 |-  ( i = 1 -> ( ( coeff ` F ) ` ( n - i ) ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
118 117 sumsn 
 |-  ( ( 1 e. RR /\ ( ( coeff ` F ) ` ( n - 1 ) ) e. CC ) -> sum_ i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
119 3 116 118 sylancr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
120 112 119 eqtr3d 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
121 84 89 120 syl2anc 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
122 60 61 83 121 ifbothda 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) )
123 59 122 eqtrd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) if ( i = 1 , ( 1 x. ( ( coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( ( coeff ` F ) ` ( n - i ) ) ) ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) )
124 37 45 123 3eqtrd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( ( coeff ` ( Xp oF x. F ) ) ` n ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) )
125 30 124 eqtrd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( ( coeff ` ( F oF x. Xp ) ) ` n ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) )
126 125 mpteq2dva 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( n e. NN0 |-> ( ( coeff ` ( F oF x. Xp ) ) ` n ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )
127 16 126 eqtrd 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )