Metamath Proof Explorer

Theorem coe1tmmul2

Description: Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-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 coe1tmmul2 
|- ( ph -> ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .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 /\ A e. B /\ ( C .x. ( D .^ X ) ) e. B ) -> ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) ) )
18 12 11 16 17 syl3anc 
 |-  ( ph -> ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) ) )
19 eqeq2 
 |-  ( ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) = if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) -> ( ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) <-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )
20 eqeq2 
 |-  ( .0. = if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) -> ( ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = .0. <-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )
21 12 adantr 
 |-  ( ( 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 ovex 
 |-  ( 0 ... x ) e. _V
25 24 a1i 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( 0 ... x ) e. _V )
26 simprr 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> D <_ x )
27 14 adantr 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> D e. NN0 )
28 simprl 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> x e. NN0 )
29 nn0sub 
 |-  ( ( D e. NN0 /\ x e. NN0 ) -> ( D <_ x <-> ( x - D ) e. NN0 ) )
30 27 28 29 syl2anc 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( D <_ x <-> ( x - D ) e. NN0 ) )
31 26 30 mpbid 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( x - D ) e. NN0 )
32 27 nn0ge0d 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> 0 <_ D )
33 nn0re 
 |-  ( x e. NN0 -> x e. RR )
34 33 ad2antrl 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> x e. RR )
35 14 nn0red 
 |-  ( ph -> D e. RR )
36 35 adantr 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> D e. RR )
37 34 36 subge02d 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( 0 <_ D <-> ( x - D ) <_ x ) )
38 32 37 mpbid 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( x - D ) <_ x )
39 fznn0 
 |-  ( x e. NN0 -> ( ( x - D ) e. ( 0 ... x ) <-> ( ( x - D ) e. NN0 /\ ( x - D ) <_ x ) ) )
40 39 ad2antrl 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( x - D ) e. ( 0 ... x ) <-> ( ( x - D ) e. NN0 /\ ( x - D ) <_ x ) ) )
41 31 38 40 mpbir2and 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( x - D ) e. ( 0 ... x ) )
42 12 ad2antrr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> R e. Ring )
43 eqid 
 |-  ( coe1 ` A ) = ( coe1 ` A )
44 43 8 3 2 coe1f 
 |-  ( A e. B -> ( coe1 ` A ) : NN0 --> K )
45 11 44 syl 
 |-  ( ph -> ( coe1 ` A ) : NN0 --> K )
46 45 ad2antrr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( coe1 ` A ) : NN0 --> K )
47 elfznn0 
 |-  ( y e. ( 0 ... x ) -> y e. NN0 )
48 47 adantl 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> y e. NN0 )
49 46 48 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( ( coe1 ` A ) ` y ) e. K )
50 eqid 
 |-  ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( coe1 ` ( C .x. ( D .^ X ) ) )
51 50 8 3 2 coe1f 
 |-  ( ( C .x. ( D .^ X ) ) e. B -> ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K )
52 16 51 syl 
 |-  ( ph -> ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) : NN0 --> K )
54 fznn0sub 
 |-  ( y e. ( 0 ... x ) -> ( x - y ) e. NN0 )
55 54 adantl 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( x - y ) e. NN0 )
56 53 55 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) e. K )
57 2 10 ringcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` A ) ` y ) e. K /\ ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) e. K ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) e. K )
58 42 49 56 57 syl3anc 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) e. K )
59 58 fmpttd 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) : ( 0 ... x ) --> K )
60 12 ad2antrr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> R e. Ring )
61 13 ad2antrr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> C e. K )
62 14 ad2antrr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> D e. NN0 )
63 eldifi 
 |-  ( y e. ( ( 0 ... x ) \ { ( x - D ) } ) -> y e. ( 0 ... x ) )
64 63 54 syl 
 |-  ( y e. ( ( 0 ... x ) \ { ( x - D ) } ) -> ( x - y ) e. NN0 )
65 64 adantl 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> ( x - y ) e. NN0 )
66 eldifsn 
 |-  ( y e. ( ( 0 ... x ) \ { ( x - D ) } ) <-> ( y e. ( 0 ... x ) /\ y =/= ( x - D ) ) )
67 simplrl 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> x e. NN0 )
68 67 nn0cnd 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> x e. CC )
69 47 nn0cnd 
 |-  ( y e. ( 0 ... x ) -> y e. CC )
70 69 adantl 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> y e. CC )
71 68 70 nncand 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( x - ( x - y ) ) = y )
72 71 eqcomd 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> y = ( x - ( x - y ) ) )
73 oveq2 
 |-  ( D = ( x - y ) -> ( x - D ) = ( x - ( x - y ) ) )
74 73 eqeq2d 
 |-  ( D = ( x - y ) -> ( y = ( x - D ) <-> y = ( x - ( x - y ) ) ) )
75 72 74 syl5ibrcom 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( D = ( x - y ) -> y = ( x - D ) ) )
76 75 necon3d 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( y =/= ( x - D ) -> D =/= ( x - y ) ) )
77 76 impr 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ ( y e. ( 0 ... x ) /\ y =/= ( x - D ) ) ) -> D =/= ( x - y ) )
78 66 77 sylan2b 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> D =/= ( x - y ) )
79 1 2 3 4 5 6 7 60 61 62 65 78 coe1tmfv2 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) = .0. )
80 79 oveq2d 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) = ( ( ( coe1 ` A ) ` y ) .X. .0. ) )
81 2 10 1 ringrz 
 |-  ( ( R e. Ring /\ ( ( coe1 ` A ) ` y ) e. K ) -> ( ( ( coe1 ` A ) ` y ) .X. .0. ) = .0. )
82 42 49 81 syl2anc 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( 0 ... x ) ) -> ( ( ( coe1 ` A ) ` y ) .X. .0. ) = .0. )
83 63 82 sylan2 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> ( ( ( coe1 ` A ) ` y ) .X. .0. ) = .0. )
84 80 83 eqtrd 
 |-  ( ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) /\ y e. ( ( 0 ... x ) \ { ( x - D ) } ) ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) = .0. )
85 84 25 suppss2 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) supp .0. ) C_ { ( x - D ) } )
86 2 1 23 25 41 59 85 gsumpt 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ` ( x - D ) ) )
87 fveq2 
 |-  ( y = ( x - D ) -> ( ( coe1 ` A ) ` y ) = ( ( coe1 ` A ) ` ( x - D ) ) )
88 oveq2 
 |-  ( y = ( x - D ) -> ( x - y ) = ( x - ( x - D ) ) )
89 88 fveq2d 
 |-  ( y = ( x - D ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) = ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) )
90 87 89 oveq12d 
 |-  ( y = ( x - D ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) ) )
91 eqid 
 |-  ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) = ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) )
92 ovex 
 |-  ( ( ( coe1 ` A ) ` ( x - D ) ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) ) e. _V
93 90 91 92 fvmpt 
 |-  ( ( x - D ) e. ( 0 ... x ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ` ( x - D ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) ) )
94 41 93 syl 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ` ( x - D ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) ) )
95 28 nn0cnd 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> x e. CC )
96 27 nn0cnd 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> D e. CC )
97 95 96 nncand 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( x - ( x - D ) ) = D )
98 97 fveq2d 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) = ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) )
99 13 adantr 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> C e. K )
100 1 2 3 4 5 6 7 coe1tmfv1 
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
101 21 99 27 100 syl3anc 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
102 98 101 eqtrd 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) = C )
103 102 oveq2d 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( ( ( coe1 ` A ) ` ( x - D ) ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - ( x - D ) ) ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) )
104 86 94 103 3eqtrd 
 |-  ( ( ph /\ ( x e. NN0 /\ D <_ x ) ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) )
105 104 anassrs 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) )
106 12 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> R e. Ring )
107 13 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> C e. K )
108 14 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> D e. NN0 )
109 54 ad2antll 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( x - y ) e. NN0 )
110 54 nn0red 
 |-  ( y e. ( 0 ... x ) -> ( x - y ) e. RR )
111 110 ad2antll 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( x - y ) e. RR )
112 33 ad2antlr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> x e. RR )
113 35 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> D e. RR )
114 47 ad2antll 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> y e. NN0 )
115 114 nn0ge0d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> 0 <_ y )
116 47 nn0red 
 |-  ( y e. ( 0 ... x ) -> y e. RR )
117 116 ad2antll 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> y e. RR )
118 112 117 subge02d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( 0 <_ y <-> ( x - y ) <_ x ) )
119 115 118 mpbid 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( x - y ) <_ x )
120 simprl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> -. D <_ x )
121 112 113 ltnled 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( x < D <-> -. D <_ x ) )
122 120 121 mpbird 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> x < D )
123 111 112 113 119 122 lelttrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( x - y ) < D )
124 111 123 gtned 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> D =/= ( x - y ) )
125 1 2 3 4 5 6 7 106 107 108 109 124 coe1tmfv2 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) = .0. )
126 125 oveq2d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) = ( ( ( coe1 ` A ) ` y ) .X. .0. ) )
127 45 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( coe1 ` A ) : NN0 --> K )
128 127 114 ffvelcdmd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( ( coe1 ` A ) ` y ) e. K )
129 106 128 81 syl2anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( ( ( coe1 ` A ) ` y ) .X. .0. ) = .0. )
130 126 129 eqtrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ ( -. D <_ x /\ y e. ( 0 ... x ) ) ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) = .0. )
131 130 anassrs 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) /\ y e. ( 0 ... x ) ) -> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) = .0. )
132 131 mpteq2dva 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) = ( y e. ( 0 ... x ) |-> .0. ) )
133 132 oveq2d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) )
134 12 22 syl 
 |-  ( ph -> R e. Mnd )
135 1 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... x ) e. _V ) -> ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) = .0. )
136 134 24 135 sylancl 
 |-  ( ph -> ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) = .0. )
137 136 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> .0. ) ) = .0. )
138 133 137 eqtrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ -. D <_ x ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = .0. )
139 19 20 105 138 ifbothda 
 |-  ( ( ph /\ x e. NN0 ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) = if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) )
140 139 mpteq2dva 
 |-  ( ph -> ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` A ) ` y ) .X. ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` ( x - y ) ) ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )
141 18 140 eqtrd 
 |-  ( ph -> ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )