Metamath Proof Explorer

Theorem gsummoncoe1

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019)

Ref Expression
Hypotheses gsummonply1.p 
|- P = ( Poly1 ` R )
gsummonply1.b 
|- B = ( Base ` P )
gsummonply1.x 
|- X = ( var1 ` R )
gsummonply1.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
gsummonply1.r 
|- ( ph -> R e. Ring )
gsummonply1.k 
|- K = ( Base ` R )
gsummonply1.m 
|- .* = ( .s ` P )
gsummonply1.0 
|- .0. = ( 0g ` R )
gsummonply1.a 
|- ( ph -> A. k e. NN0 A e. K )
gsummonply1.f 
|- ( ph -> ( k e. NN0 |-> A ) finSupp .0. )
gsummonply1.l 
|- ( ph -> L e. NN0 )
Assertion gsummoncoe1 
|- ( ph -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A )

Proof

Step Hyp Ref Expression
1 gsummonply1.p 
 |-  P = ( Poly1 ` R )
2 gsummonply1.b 
 |-  B = ( Base ` P )
3 gsummonply1.x 
 |-  X = ( var1 ` R )
4 gsummonply1.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
5 gsummonply1.r 
 |-  ( ph -> R e. Ring )
6 gsummonply1.k 
 |-  K = ( Base ` R )
7 gsummonply1.m 
 |-  .* = ( .s ` P )
8 gsummonply1.0 
 |-  .0. = ( 0g ` R )
9 gsummonply1.a 
 |-  ( ph -> A. k e. NN0 A e. K )
10 gsummonply1.f 
 |-  ( ph -> ( k e. NN0 |-> A ) finSupp .0. )
11 gsummonply1.l 
 |-  ( ph -> L e. NN0 )
12 9 r19.21bi 
 |-  ( ( ph /\ k e. NN0 ) -> A e. K )
13 12 fmpttd 
 |-  ( ph -> ( k e. NN0 |-> A ) : NN0 --> K )
14 6 fvexi 
 |-  K e. _V
15 14 a1i 
 |-  ( ph -> K e. _V )
16 nn0ex 
 |-  NN0 e. _V
17 elmapg 
 |-  ( ( K e. _V /\ NN0 e. _V ) -> ( ( k e. NN0 |-> A ) e. ( K ^m NN0 ) <-> ( k e. NN0 |-> A ) : NN0 --> K ) )
18 15 16 17 sylancl 
 |-  ( ph -> ( ( k e. NN0 |-> A ) e. ( K ^m NN0 ) <-> ( k e. NN0 |-> A ) : NN0 --> K ) )
19 13 18 mpbird 
 |-  ( ph -> ( k e. NN0 |-> A ) e. ( K ^m NN0 ) )
20 8 fvexi 
 |-  .0. e. _V
21 fsuppmapnn0ub 
 |-  ( ( ( k e. NN0 |-> A ) e. ( K ^m NN0 ) /\ .0. e. _V ) -> ( ( k e. NN0 |-> A ) finSupp .0. -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) ) )
22 19 20 21 sylancl 
 |-  ( ph -> ( ( k e. NN0 |-> A ) finSupp .0. -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) ) )
23 10 22 mpd 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) )
24 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> x e. NN0 )
25 9 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> A. k e. NN0 A e. K )
26 rspcsbela 
 |-  ( ( x e. NN0 /\ A. k e. NN0 A e. K ) -> [_ x / k ]_ A e. K )
27 24 25 26 syl2anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> [_ x / k ]_ A e. K )
28 eqid 
 |-  ( k e. NN0 |-> A ) = ( k e. NN0 |-> A )
29 28 fvmpts 
 |-  ( ( x e. NN0 /\ [_ x / k ]_ A e. K ) -> ( ( k e. NN0 |-> A ) ` x ) = [_ x / k ]_ A )
30 24 27 29 syl2anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( k e. NN0 |-> A ) ` x ) = [_ x / k ]_ A )
31 30 eqeq1d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( ( k e. NN0 |-> A ) ` x ) = .0. <-> [_ x / k ]_ A = .0. ) )
32 31 imbi2d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) <-> ( s < x -> [_ x / k ]_ A = .0. ) ) )
33 32 biimpd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) -> ( s < x -> [_ x / k ]_ A = .0. ) ) )
34 33 ralimdva 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) -> A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) )
35 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
36 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
37 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
38 5 36 37 3syl 
 |-  ( ph -> P e. CMnd )
39 38 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> P e. CMnd )
40 5 3ad2ant1 
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> R e. Ring )
41 simp3 
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> A e. K )
42 simp2 
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> k e. NN0 )
43 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
44 6 1 3 7 43 4 2 ply1tmcl 
 |-  ( ( R e. Ring /\ A e. K /\ k e. NN0 ) -> ( A .* ( k .^ X ) ) e. B )
45 40 41 42 44 syl3anc 
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> ( A .* ( k .^ X ) ) e. B )
46 45 3expia 
 |-  ( ( ph /\ k e. NN0 ) -> ( A e. K -> ( A .* ( k .^ X ) ) e. B ) )
47 46 ralimdva 
 |-  ( ph -> ( A. k e. NN0 A e. K -> A. k e. NN0 ( A .* ( k .^ X ) ) e. B ) )
48 9 47 mpd 
 |-  ( ph -> A. k e. NN0 ( A .* ( k .^ X ) ) e. B )
49 48 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> A. k e. NN0 ( A .* ( k .^ X ) ) e. B )
50 simplr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> s e. NN0 )
51 nfv 
 |-  F/ k s < x
52 nfcsb1v 
 |-  F/_ k [_ x / k ]_ A
53 52 nfeq1 
 |-  F/ k [_ x / k ]_ A = .0.
54 51 53 nfim 
 |-  F/ k ( s < x -> [_ x / k ]_ A = .0. )
55 nfv 
 |-  F/ x ( s < k -> [_ k / k ]_ A = .0. )
56 breq2 
 |-  ( x = k -> ( s < x <-> s < k ) )
57 csbeq1 
 |-  ( x = k -> [_ x / k ]_ A = [_ k / k ]_ A )
58 57 eqeq1d 
 |-  ( x = k -> ( [_ x / k ]_ A = .0. <-> [_ k / k ]_ A = .0. ) )
59 56 58 imbi12d 
 |-  ( x = k -> ( ( s < x -> [_ x / k ]_ A = .0. ) <-> ( s < k -> [_ k / k ]_ A = .0. ) ) )
60 54 55 59 cbvralw 
 |-  ( A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) <-> A. k e. NN0 ( s < k -> [_ k / k ]_ A = .0. ) )
61 csbid 
 |-  [_ k / k ]_ A = A
62 61 eqeq1i 
 |-  ( [_ k / k ]_ A = .0. <-> A = .0. )
63 oveq1 
 |-  ( A = .0. -> ( A .* ( k .^ X ) ) = ( .0. .* ( k .^ X ) ) )
64 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
65 5 64 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
66 65 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
67 8 66 eqtrid 
 |-  ( ph -> .0. = ( 0g ` ( Scalar ` P ) ) )
68 67 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> .0. = ( 0g ` ( Scalar ` P ) ) )
69 68 oveq1d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( .0. .* ( k .^ X ) ) = ( ( 0g ` ( Scalar ` P ) ) .* ( k .^ X ) ) )
70 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
71 5 70 syl 
 |-  ( ph -> P e. LMod )
72 71 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> P e. LMod )
73 43 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
74 5 36 73 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
75 74 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
76 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> k e. NN0 )
77 eqid 
 |-  ( Base ` P ) = ( Base ` P )
78 3 1 77 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
79 5 78 syl 
 |-  ( ph -> X e. ( Base ` P ) )
80 79 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> X e. ( Base ` P ) )
81 43 77 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
82 81 4 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ k e. NN0 /\ X e. ( Base ` P ) ) -> ( k .^ X ) e. ( Base ` P ) )
83 75 76 80 82 syl3anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` P ) )
84 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
85 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
86 77 84 7 85 35 lmod0vs 
 |-  ( ( P e. LMod /\ ( k .^ X ) e. ( Base ` P ) ) -> ( ( 0g ` ( Scalar ` P ) ) .* ( k .^ X ) ) = ( 0g ` P ) )
87 72 83 86 syl2anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( ( 0g ` ( Scalar ` P ) ) .* ( k .^ X ) ) = ( 0g ` P ) )
88 69 87 eqtrd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( .0. .* ( k .^ X ) ) = ( 0g ` P ) )
89 63 88 sylan9eqr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) /\ A = .0. ) -> ( A .* ( k .^ X ) ) = ( 0g ` P ) )
90 89 ex 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( A = .0. -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) )
91 62 90 syl5bi 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( [_ k / k ]_ A = .0. -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) )
92 91 imim2d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( ( s < k -> [_ k / k ]_ A = .0. ) -> ( s < k -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) ) )
93 92 ralimdva 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. k e. NN0 ( s < k -> [_ k / k ]_ A = .0. ) -> A. k e. NN0 ( s < k -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) ) )
94 60 93 syl5bi 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) -> A. k e. NN0 ( s < k -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) ) )
95 94 imp 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> A. k e. NN0 ( s < k -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) )
96 2 35 39 49 50 95 gsummptnn0fz 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) = ( P gsum ( k e. ( 0 ... s ) |-> ( A .* ( k .^ X ) ) ) ) )
97 96 fveq2d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. ( 0 ... s ) |-> ( A .* ( k .^ X ) ) ) ) ) )
98 97 fveq1d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = ( ( coe1 ` ( P gsum ( k e. ( 0 ... s ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) )
99 5 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> R e. Ring )
100 11 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> L e. NN0 )
101 elfznn0 
 |-  ( k e. ( 0 ... s ) -> k e. NN0 )
102 simpll 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ph )
103 12 adantlr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> A e. K )
104 102 76 103 3jca 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( ph /\ k e. NN0 /\ A e. K ) )
105 101 104 sylan2 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. ( 0 ... s ) ) -> ( ph /\ k e. NN0 /\ A e. K ) )
106 105 45 syl 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. ( 0 ... s ) ) -> ( A .* ( k .^ X ) ) e. B )
107 106 ralrimiva 
 |-  ( ( ph /\ s e. NN0 ) -> A. k e. ( 0 ... s ) ( A .* ( k .^ X ) ) e. B )
108 107 adantr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> A. k e. ( 0 ... s ) ( A .* ( k .^ X ) ) e. B )
109 fzfid 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( 0 ... s ) e. Fin )
110 1 2 99 100 108 109 coe1fzgsumd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( ( coe1 ` ( P gsum ( k e. ( 0 ... s ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( A .* ( k .^ X ) ) ) ` L ) ) ) )
111 nfv 
 |-  F/ k ( ph /\ s e. NN0 )
112 nfcv 
 |-  F/_ k NN0
113 112 54 nfralw 
 |-  F/ k A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. )
114 111 113 nfan 
 |-  F/ k ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) )
115 5 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> R e. Ring )
116 12 expcom 
 |-  ( k e. NN0 -> ( ph -> A e. K ) )
117 116 101 syl11 
 |-  ( ph -> ( k e. ( 0 ... s ) -> A e. K ) )
118 117 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( k e. ( 0 ... s ) -> A e. K ) )
119 118 imp 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> A e. K )
120 101 adantl 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> k e. NN0 )
121 8 6 1 3 7 43 4 coe1tm 
 |-  ( ( R e. Ring /\ A e. K /\ k e. NN0 ) -> ( coe1 ` ( A .* ( k .^ X ) ) ) = ( n e. NN0 |-> if ( n = k , A , .0. ) ) )
122 115 119 120 121 syl3anc 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> ( coe1 ` ( A .* ( k .^ X ) ) ) = ( n e. NN0 |-> if ( n = k , A , .0. ) ) )
123 eqeq1 
 |-  ( n = L -> ( n = k <-> L = k ) )
124 123 ifbid 
 |-  ( n = L -> if ( n = k , A , .0. ) = if ( L = k , A , .0. ) )
125 124 adantl 
 |-  ( ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) /\ n = L ) -> if ( n = k , A , .0. ) = if ( L = k , A , .0. ) )
126 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> L e. NN0 )
127 6 8 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
128 5 127 syl 
 |-  ( ph -> .0. e. K )
129 128 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> .0. e. K )
130 119 129 ifcld 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> if ( L = k , A , .0. ) e. K )
131 122 125 126 130 fvmptd 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> ( ( coe1 ` ( A .* ( k .^ X ) ) ) ` L ) = if ( L = k , A , .0. ) )
132 114 131 mpteq2da 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( A .* ( k .^ X ) ) ) ` L ) ) = ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) )
133 132 oveq2d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( A .* ( k .^ X ) ) ) ` L ) ) ) = ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) )
134 breq2 
 |-  ( x = L -> ( s < x <-> s < L ) )
135 csbeq1 
 |-  ( x = L -> [_ x / k ]_ A = [_ L / k ]_ A )
136 135 eqeq1d 
 |-  ( x = L -> ( [_ x / k ]_ A = .0. <-> [_ L / k ]_ A = .0. ) )
137 134 136 imbi12d 
 |-  ( x = L -> ( ( s < x -> [_ x / k ]_ A = .0. ) <-> ( s < L -> [_ L / k ]_ A = .0. ) ) )
138 137 rspcva 
 |-  ( ( L e. NN0 /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( s < L -> [_ L / k ]_ A = .0. ) )
139 nfv 
 |-  F/ k ( ph /\ ( s e. NN0 /\ s < L ) )
140 nfcsb1v 
 |-  F/_ k [_ L / k ]_ A
141 140 nfeq1 
 |-  F/ k [_ L / k ]_ A = .0.
142 139 141 nfan 
 |-  F/ k ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. )
143 elfz2nn0 
 |-  ( k e. ( 0 ... s ) <-> ( k e. NN0 /\ s e. NN0 /\ k <_ s ) )
144 nn0re 
 |-  ( k e. NN0 -> k e. RR )
145 144 ad2antrr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> k e. RR )
146 nn0re 
 |-  ( s e. NN0 -> s e. RR )
147 146 adantl 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> s e. RR )
148 147 adantr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> s e. RR )
149 nn0re 
 |-  ( L e. NN0 -> L e. RR )
150 149 adantl 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> L e. RR )
151 lelttr 
 |-  ( ( k e. RR /\ s e. RR /\ L e. RR ) -> ( ( k <_ s /\ s < L ) -> k < L ) )
152 145 148 150 151 syl3anc 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( ( k <_ s /\ s < L ) -> k < L ) )
153 animorr 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> ( L < k \/ k < L ) )
154 df-ne 
 |-  ( L =/= k <-> -. L = k )
155 144 adantr 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> k e. RR )
156 lttri2 
 |-  ( ( L e. RR /\ k e. RR ) -> ( L =/= k <-> ( L < k \/ k < L ) ) )
157 149 155 156 syl2anr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( L =/= k <-> ( L < k \/ k < L ) ) )
158 157 adantr 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> ( L =/= k <-> ( L < k \/ k < L ) ) )
159 154 158 bitr3id 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> ( -. L = k <-> ( L < k \/ k < L ) ) )
160 153 159 mpbird 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> -. L = k )
161 160 ex 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( k < L -> -. L = k ) )
162 152 161 syld 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( ( k <_ s /\ s < L ) -> -. L = k ) )
163 162 exp4b 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> ( L e. NN0 -> ( k <_ s -> ( s < L -> -. L = k ) ) ) )
164 163 expimpd 
 |-  ( k e. NN0 -> ( ( s e. NN0 /\ L e. NN0 ) -> ( k <_ s -> ( s < L -> -. L = k ) ) ) )
165 164 com23 
 |-  ( k e. NN0 -> ( k <_ s -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) ) )
166 165 imp 
 |-  ( ( k e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) )
167 166 3adant2 
 |-  ( ( k e. NN0 /\ s e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) )
168 143 167 sylbi 
 |-  ( k e. ( 0 ... s ) -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) )
169 168 expd 
 |-  ( k e. ( 0 ... s ) -> ( s e. NN0 -> ( L e. NN0 -> ( s < L -> -. L = k ) ) ) )
170 11 169 syl7 
 |-  ( k e. ( 0 ... s ) -> ( s e. NN0 -> ( ph -> ( s < L -> -. L = k ) ) ) )
171 170 com12 
 |-  ( s e. NN0 -> ( k e. ( 0 ... s ) -> ( ph -> ( s < L -> -. L = k ) ) ) )
172 171 com24 
 |-  ( s e. NN0 -> ( s < L -> ( ph -> ( k e. ( 0 ... s ) -> -. L = k ) ) ) )
173 172 imp 
 |-  ( ( s e. NN0 /\ s < L ) -> ( ph -> ( k e. ( 0 ... s ) -> -. L = k ) ) )
174 173 impcom 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> ( k e. ( 0 ... s ) -> -. L = k ) )
175 174 adantr 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( k e. ( 0 ... s ) -> -. L = k ) )
176 175 imp 
 |-  ( ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) /\ k e. ( 0 ... s ) ) -> -. L = k )
177 176 iffalsed 
 |-  ( ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) /\ k e. ( 0 ... s ) ) -> if ( L = k , A , .0. ) = .0. )
178 142 177 mpteq2da 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) = ( k e. ( 0 ... s ) |-> .0. ) )
179 178 oveq2d 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) )
180 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
181 5 180 syl 
 |-  ( ph -> R e. Mnd )
182 181 adantr 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> R e. Mnd )
183 ovex 
 |-  ( 0 ... s ) e. _V
184 8 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... s ) e. _V ) -> ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) = .0. )
185 182 183 184 sylancl 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) = .0. )
186 185 adantr 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) = .0. )
187 id 
 |-  ( [_ L / k ]_ A = .0. -> [_ L / k ]_ A = .0. )
188 187 eqcomd 
 |-  ( [_ L / k ]_ A = .0. -> .0. = [_ L / k ]_ A )
189 188 adantl 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> .0. = [_ L / k ]_ A )
190 179 186 189 3eqtrd 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A )
191 190 ex 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> ( [_ L / k ]_ A = .0. -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) )
192 191 expr 
 |-  ( ( ph /\ s e. NN0 ) -> ( s < L -> ( [_ L / k ]_ A = .0. -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) )
193 192 a2d 
 |-  ( ( ph /\ s e. NN0 ) -> ( ( s < L -> [_ L / k ]_ A = .0. ) -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) )
194 193 ex 
 |-  ( ph -> ( s e. NN0 -> ( ( s < L -> [_ L / k ]_ A = .0. ) -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) ) )
195 194 com13 
 |-  ( ( s < L -> [_ L / k ]_ A = .0. ) -> ( s e. NN0 -> ( ph -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) ) )
196 138 195 syl 
 |-  ( ( L e. NN0 /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( s e. NN0 -> ( ph -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) ) )
197 196 ex 
 |-  ( L e. NN0 -> ( A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) -> ( s e. NN0 -> ( ph -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) ) ) )
198 197 com24 
 |-  ( L e. NN0 -> ( ph -> ( s e. NN0 -> ( A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) ) ) )
199 11 198 mpcom 
 |-  ( ph -> ( s e. NN0 -> ( A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) ) ) )
200 199 imp31 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( s < L -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) )
201 200 com12 
 |-  ( s < L -> ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) )
202 pm3.2 
 |-  ( ( ph /\ s e. NN0 ) -> ( -. s < L -> ( ( ph /\ s e. NN0 ) /\ -. s < L ) ) )
203 202 adantr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( -. s < L -> ( ( ph /\ s e. NN0 ) /\ -. s < L ) ) )
204 181 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> R e. Mnd )
205 183 a1i 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> ( 0 ... s ) e. _V )
206 11 nn0red 
 |-  ( ph -> L e. RR )
207 lenlt 
 |-  ( ( L e. RR /\ s e. RR ) -> ( L <_ s <-> -. s < L ) )
208 206 146 207 syl2an 
 |-  ( ( ph /\ s e. NN0 ) -> ( L <_ s <-> -. s < L ) )
209 11 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> L e. NN0 )
210 simplr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> s e. NN0 )
211 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> L <_ s )
212 elfz2nn0 
 |-  ( L e. ( 0 ... s ) <-> ( L e. NN0 /\ s e. NN0 /\ L <_ s ) )
213 209 210 211 212 syl3anbrc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> L e. ( 0 ... s ) )
214 213 ex 
 |-  ( ( ph /\ s e. NN0 ) -> ( L <_ s -> L e. ( 0 ... s ) ) )
215 208 214 sylbird 
 |-  ( ( ph /\ s e. NN0 ) -> ( -. s < L -> L e. ( 0 ... s ) ) )
216 215 imp 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> L e. ( 0 ... s ) )
217 eqcom 
 |-  ( L = k <-> k = L )
218 ifbi 
 |-  ( ( L = k <-> k = L ) -> if ( L = k , A , .0. ) = if ( k = L , A , .0. ) )
219 217 218 ax-mp 
 |-  if ( L = k , A , .0. ) = if ( k = L , A , .0. )
220 219 mpteq2i 
 |-  ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) = ( k e. ( 0 ... s ) |-> if ( k = L , A , .0. ) )
221 12 6 eleqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> A e. ( Base ` R ) )
222 221 ex 
 |-  ( ph -> ( k e. NN0 -> A e. ( Base ` R ) ) )
223 222 adantr 
 |-  ( ( ph /\ s e. NN0 ) -> ( k e. NN0 -> A e. ( Base ` R ) ) )
224 223 101 impel 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. ( 0 ... s ) ) -> A e. ( Base ` R ) )
225 224 ralrimiva 
 |-  ( ( ph /\ s e. NN0 ) -> A. k e. ( 0 ... s ) A e. ( Base ` R ) )
226 225 adantr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> A. k e. ( 0 ... s ) A e. ( Base ` R ) )
227 8 204 205 216 220 226 gsummpt1n0 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A )
228 203 227 syl6com 
 |-  ( -. s < L -> ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A ) )
229 201 228 pm2.61i 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A )
230 133 229 eqtrd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( ( coe1 ` ( A .* ( k .^ X ) ) ) ` L ) ) ) = [_ L / k ]_ A )
231 98 110 230 3eqtrd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A )
232 231 ex 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A ) )
233 34 232 syld 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A ) )
234 233 rexlimdva 
 |-  ( ph -> ( E. s e. NN0 A. x e. NN0 ( s < x -> ( ( k e. NN0 |-> A ) ` x ) = .0. ) -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A ) )
235 23 234 mpd 
 |-  ( ph -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A )