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 ffvelrnd 
 |-  ( ( ( 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 mulid2d 
 |-  ( ( ( 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 68 72 syl 
 |-  ( ( n = 0 /\ i e. { 0 } ) -> -. i = 1 )
74 47 notbii 
 |-  ( -. i = 1 <-> -. i e. { 1 } )
75 74 biimpi 
 |-  ( -. i = 1 -> -. i e. { 1 } )
76 iffalse 
 |-  ( -. i e. { 1 } -> if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
77 73 75 76 3syl 
 |-  ( ( n = 0 /\ i e. { 0 } ) -> if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
78 66 77 sumeq12rdv 
 |-  ( n = 0 -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = sum_ i e. { 0 } 0 )
79 snfi 
 |-  { 0 } e. Fin
80 79 olci 
 |-  ( { 0 } C_ ( ZZ>= ` 0 ) \/ { 0 } e. Fin )
81 sumz 
 |-  ( ( { 0 } C_ ( ZZ>= ` 0 ) \/ { 0 } e. Fin ) -> sum_ i e. { 0 } 0 = 0 )
82 80 81 ax-mp 
 |-  sum_ i e. { 0 } 0 = 0
83 78 82 eqtrdi 
 |-  ( n = 0 -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( ( coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
84 83 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 )
85 simpll 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> F e. ( ( Poly ` RR ) \ { 0p } ) )
86 33 adantr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN0 )
87 simpr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> -. n = 0 )
88 87 neqned 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n =/= 0 )
89 elnnne0 
 |-  ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
90 86 88 89 sylanbrc 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
91 1nn0 
 |-  1 e. NN0
92 91 a1i 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 e. NN0 )
93 simpr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> n e. NN )
94 93 nnnn0d 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> n e. NN0 )
95 93 nnge1d 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 <_ n )
96 elfz2nn0 
 |-  ( 1 e. ( 0 ... n ) <-> ( 1 e. NN0 /\ n e. NN0 /\ 1 <_ n ) )
97 92 94 95 96 syl3anbrc 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 e. ( 0 ... n ) )
98 97 snssd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> { 1 } C_ ( 0 ... n ) )
99 50 ad2antrr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( coeff ` F ) : NN0 --> RR )
100 oveq2 
 |-  ( i = 1 -> ( n - i ) = ( n - 1 ) )
101 46 100 sylbi 
 |-  ( i e. { 1 } -> ( n - i ) = ( n - 1 ) )
102 101 adantl 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - i ) = ( n - 1 ) )
103 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
104 103 ad2antlr 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - 1 ) e. NN0 )
105 102 104 eqeltrd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - i ) e. NN0 )
106 99 105 ffvelrnd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( ( coeff ` F ) ` ( n - i ) ) e. RR )
107 106 recnd 
 |-  ( ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( ( coeff ` F ) ` ( n - i ) ) e. CC )
108 107 ralrimiva 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> A. i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) e. CC )
109 fzfi 
 |-  ( 0 ... n ) e. Fin
110 109 olci 
 |-  ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin )
111 110 a1i 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin ) )
112 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 ) )
113 98 108 111 112 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 ) )
114 50 adantr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( coeff ` F ) : NN0 --> RR )
115 103 adantl 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( n - 1 ) e. NN0 )
116 114 115 ffvelrnd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( coeff ` F ) ` ( n - 1 ) ) e. RR )
117 116 recnd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( coeff ` F ) ` ( n - 1 ) ) e. CC )
118 100 fveq2d 
 |-  ( i = 1 -> ( ( coeff ` F ) ` ( n - i ) ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
119 118 sumsn 
 |-  ( ( 1 e. RR /\ ( ( coeff ` F ) ` ( n - 1 ) ) e. CC ) -> sum_ i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
120 3 117 119 sylancr 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. { 1 } ( ( coeff ` F ) ` ( n - i ) ) = ( ( coeff ` F ) ` ( n - 1 ) ) )
121 113 120 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 ) ) )
122 85 90 121 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 ) ) )
123 60 61 84 122 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 ) ) ) )
124 59 123 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 ) ) ) )
125 37 45 124 3eqtrd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( ( coeff ` ( Xp oF x. F ) ) ` n ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) )
126 30 125 eqtrd 
 |-  ( ( F e. ( ( Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( ( coeff ` ( F oF x. Xp ) ) ` n ) = if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) )
127 126 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 ) ) ) ) )
128 16 127 eqtrd 
 |-  ( F e. ( ( Poly ` RR ) \ { 0p } ) -> ( coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( ( coeff ` F ) ` ( n - 1 ) ) ) ) )