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 ffvelrnd
 |-  ( ( ( 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 ffvelrnd
 |-  ( ( ( 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 ffvelrnd
 |-  ( ( ( 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. ) ) )