Metamath Proof Explorer

Theorem coe1tmmul

Description: Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses coe1tm.z 
|- .0. = ( 0g ` R )
coe1tm.k 
|- K = ( Base ` R )
coe1tm.p 
|- P = ( Poly1 ` R )
coe1tm.x 
|- X = ( var1 ` R )
coe1tm.m 
|- .x. = ( .s ` P )
coe1tm.n 
|- N = ( mulGrp ` P )
coe1tm.e 
|- .^ = ( .g ` N )
coe1tmmul.b 
|- B = ( Base ` P )
coe1tmmul.t 
|- .xb = ( .r ` P )
coe1tmmul.u 
|- .X. = ( .r ` R )
coe1tmmul.a 
|- ( ph -> A e. B )
coe1tmmul.r 
|- ( ph -> R e. Ring )
coe1tmmul.c 
|- ( ph -> C e. K )
coe1tmmul.d 
|- ( ph -> D e. NN0 )
Assertion coe1tmmul 
|- ( ph -> ( coe1 ` ( ( C .x. ( D .^ X ) ) .xb A ) ) = ( x e. NN0 |-> if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )

Proof

Step Hyp Ref Expression
1 coe1tm.z 
 |-  .0. = ( 0g ` R )
2 coe1tm.k 
 |-  K = ( Base ` R )
3 coe1tm.p 
 |-  P = ( Poly1 ` R )
4 coe1tm.x 
 |-  X = ( var1 ` R )
5 coe1tm.m 
 |-  .x. = ( .s ` P )
6 coe1tm.n 
 |-  N = ( mulGrp ` P )
7 coe1tm.e 
 |-  .^ = ( .g ` N )
8 coe1tmmul.b 
 |-  B = ( Base ` P )
9 coe1tmmul.t 
 |-  .xb = ( .r ` P )
10 coe1tmmul.u 
 |-  .X. = ( .r ` R )
11 coe1tmmul.a 
 |-  ( ph -> A e. B )
12 coe1tmmul.r 
 |-  ( ph -> R e. Ring )
13 coe1tmmul.c 
 |-  ( ph -> C e. K )
14 coe1tmmul.d 
 |-  ( ph -> D e. NN0 )
15 2 3 4 5 6 7 8 ply1tmcl 
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) e. B )
16 12 13 14 15 syl3anc 
 |-  ( ph -> ( C .x. ( D .^ X ) ) e. B )
17 3 9 10 8 coe1mul 
 |-  ( ( R e. Ring /\ ( C .x. ( D .^ X ) ) e. B /\ A e. B ) -> ( coe1 ` ( ( C .x. ( D .^ X ) ) .xb A ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) ) )
18 12 16 11 17 syl3anc 
 |-  ( ph -> ( coe1 ` ( ( C .x. ( D .^ X ) ) .xb A ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) ) )
19 eqeq2 
 |-  ( ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) = if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) -> ( ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) <-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )
20 eqeq2 
 |-  ( .0. = if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) -> ( ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = .0. <-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )
21 12 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> R e. Ring )
22 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
23 21 22 syl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> R e. Mnd )
24 ovexd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( 0 ... x ) e. _V )
25 14 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D e. NN0 )
26 simpr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D <_ x )
27 fznn0 
 |-  ( x e. NN0 -> ( D e. ( 0 ... x ) <-> ( D e. NN0 /\ D <_ x ) ) )
28 27 ad2antlr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( D e. ( 0 ... x ) <-> ( D e. NN0 /\ D <_ x ) ) )
29 25 26 28 mpbir2and 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D e. ( 0 ... x ) )
30 12 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> R e. Ring )
31 eqid 
 |-  ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( coe1 ` ( C .x. ( D .^ X ) ) )
32 31 8 3 2 coe1f 
 |-  ( ( C .x. ( D .^ X ) ) e. B -> ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K )
33 16 32 syl 
 |-  ( ph -> ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K )
34 33 adantr 
 |-  ( ( ph /\ x e. NN0 ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K )
35 elfznn0 
 |-  ( y e. ( 0 ... x ) -> y e. NN0 )
36 ffvelcdm 
 |-  ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K /\ y e. NN0 ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) e. K )
37 34 35 36 syl2an 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) e. K )
38 eqid 
 |-  ( coe1 ` A ) = ( coe1 ` A )
39 38 8 3 2 coe1f 
 |-  ( A e. B -> ( coe1 ` A ) : NN0 --> K )
40 11 39 syl 
 |-  ( ph -> ( coe1 ` A ) : NN0 --> K )
41 40 adantr 
 |-  ( ( ph /\ x e. NN0 ) -> ( coe1 ` A ) : NN0 --> K )
42 fznn0sub 
 |-  ( y e. ( 0 ... x ) -> ( x - y ) e. NN0 )
43 ffvelcdm 
 |-  ( ( ( coe1 ` A ) : NN0 --> K /\ ( x - y ) e. NN0 ) -> ( ( coe1 ` A ) ` ( x - y ) ) e. K )
44 41 42 43 syl2an 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> ( ( coe1 ` A ) ` ( x - y ) ) e. K )
45 2 10 ringcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) e. K /\ ( ( coe1 ` A ) ` ( x - y ) ) e. K ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) e. K )
46 30 37 44 45 syl3anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) e. K )
47 46 fmpttd 
 |-  ( ( ph /\ x e. NN0 ) -> ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) : ( 0 ... x ) --> K )
48 47 adantr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) : ( 0 ... x ) --> K )
49 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> R e. Ring )
50 13 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> C e. K )
51 14 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> D e. NN0 )
52 eldifi 
 |-  ( y e. ( ( 0 ... x ) \ { D } ) -> y e. ( 0 ... x ) )
53 52 35 syl 
 |-  ( y e. ( ( 0 ... x ) \ { D } ) -> y e. NN0 )
54 53 adantl 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> y e. NN0 )
55 eldifsni 
 |-  ( y e. ( ( 0 ... x ) \ { D } ) -> y =/= D )
56 55 necomd 
 |-  ( y e. ( ( 0 ... x ) \ { D } ) -> D =/= y )
57 56 adantl 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> D =/= y )
58 1 2 3 4 5 6 7 49 50 51 54 57 coe1tmfv2 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) = .0. )
59 58 oveq1d 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) )
60 2 10 1 ringlz 
 |-  ( ( R e. Ring /\ ( ( coe1 ` A ) ` ( x - y ) ) e. K ) -> ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
61 30 44 60 syl2anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
62 52 61 sylan2 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
63 62 adantlr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
64 59 63 eqtrd 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) /\ y e. ( ( 0 ... x ) \ { D } ) ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
65 64 24 suppss2 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) supp .0. ) C_ { D } )
66 2 1 23 24 29 48 65 gsumpt 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ` D ) )
67 fveq2 
 |-  ( y = D -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) = ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) )
68 oveq2 
 |-  ( y = D -> ( x - y ) = ( x - D ) )
69 68 fveq2d 
 |-  ( y = D -> ( ( coe1 ` A ) ` ( x - y ) ) = ( ( coe1 ` A ) ` ( x - D ) ) )
70 67 69 oveq12d 
 |-  ( y = D -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) .X. ( ( coe1 ` A ) ` ( x - D ) ) ) )
71 eqid 
 |-  ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) = ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) )
72 ovex 
 |-  ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) .X. ( ( coe1 ` A ) ` ( x - D ) ) ) e. _V
73 70 71 72 fvmpt 
 |-  ( D e. ( 0 ... x ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ` D ) = ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) .X. ( ( coe1 ` A ) ` ( x - D ) ) ) )
74 29 73 syl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ` D ) = ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) .X. ( ( coe1 ` A ) ` ( x - D ) ) ) )
75 1 2 3 4 5 6 7 coe1tmfv1 
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
76 12 13 14 75 syl3anc 
 |-  ( ph -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
77 76 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
78 77 oveq1d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) .X. ( ( coe1 ` A ) ` ( x - D ) ) ) = ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) )
79 74 78 eqtrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ` D ) = ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) )
80 66 79 eqtrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) )
81 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> R e. Ring )
82 13 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> C e. K )
83 14 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> D e. NN0 )
84 35 adantl 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> y e. NN0 )
85 elfzle2 
 |-  ( y e. ( 0 ... x ) -> y <_ x )
86 85 adantl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> y <_ x )
87 breq1 
 |-  ( D = y -> ( D <_ x <-> y <_ x ) )
88 86 87 syl5ibrcom 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> ( D = y -> D <_ x ) )
89 88 necon3bd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) -> ( -. D <_ x -> D =/= y ) )
90 89 imp 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ y e. ( 0 ... x ) ) /\ -. D <_ x ) -> D =/= y )
91 90 an32s 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> D =/= y )
92 1 2 3 4 5 6 7 81 82 83 84 91 coe1tmfv2 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) = .0. )
93 92 oveq1d 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) )
94 61 adantlr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> ( .0. .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
95 93 94 eqtrd 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) = .0. )
96 95 mpteq2dva 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) = ( y e. ( 0 ... x ) |-> .0. ) )
97 96 oveq2d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) )
98 12 22 syl 
 |-  ( ph -> R e. Mnd )
99 98 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> R e. Mnd )
100 ovexd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( 0 ... x ) e. _V )
101 1 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... x ) e. _V ) -> ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) = .0. )
102 99 100 101 syl2anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) = .0. )
103 97 102 eqtrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = .0. )
104 19 20 80 103 ifbothda 
 |-  ( ( ph /\ x e. NN0 ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) = if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) )
105 104 mpteq2dva 
 |-  ( ph -> ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` y ) .X. ( ( coe1 ` A ) ` ( x - y ) ) ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )
106 18 105 eqtrd 
 |-  ( ph -> ( coe1 ` ( ( C .x. ( D .^ X ) ) .xb A ) ) = ( x e. NN0 |-> if ( D <_ x , ( C .X. ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )