This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqid 
 |-  ( Base ` P ) = ( Base ` P )
74 43 73 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
75 43 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
76 5 36 75 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
77 76 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
78 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> k e. NN0 )
79 3 1 73 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
80 5 79 syl 
 |-  ( ph -> X e. ( Base ` P ) )
81 80 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> X e. ( Base ` P ) )
82 74 4 77 78 81 mulgnn0cld 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` P ) )
83 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
84 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
85 73 83 7 84 35 lmod0vs 
 |-  ( ( P e. LMod /\ ( k .^ X ) e. ( Base ` P ) ) -> ( ( 0g ` ( Scalar ` P ) ) .* ( k .^ X ) ) = ( 0g ` P ) )
86 72 82 85 syl2anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( ( 0g ` ( Scalar ` P ) ) .* ( k .^ X ) ) = ( 0g ` P ) )
87 69 86 eqtrd 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( .0. .* ( k .^ X ) ) = ( 0g ` P ) )
88 63 87 sylan9eqr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) /\ A = .0. ) -> ( A .* ( k .^ X ) ) = ( 0g ` P ) )
89 88 ex 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( A = .0. -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) )
90 62 89 biimtrid 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( [_ k / k ]_ A = .0. -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) )
91 90 imim2d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( ( s < k -> [_ k / k ]_ A = .0. ) -> ( s < k -> ( A .* ( k .^ X ) ) = ( 0g ` P ) ) ) )
92 91 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 ) ) ) )
93 60 92 biimtrid 
 |-  ( ( 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 ) ) ) )
94 93 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 ) ) )
95 2 35 39 49 50 94 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 ) ) ) ) )
96 95 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 ) ) ) ) ) )
97 96 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 ) )
98 5 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> R e. Ring )
99 11 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> L e. NN0 )
100 elfznn0 
 |-  ( k e. ( 0 ... s ) -> k e. NN0 )
101 simpll 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ph )
102 12 adantlr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> A e. K )
103 101 78 102 3jca 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. NN0 ) -> ( ph /\ k e. NN0 /\ A e. K ) )
104 100 103 sylan2 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. ( 0 ... s ) ) -> ( ph /\ k e. NN0 /\ A e. K ) )
105 104 45 syl 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. ( 0 ... s ) ) -> ( A .* ( k .^ X ) ) e. B )
106 105 ralrimiva 
 |-  ( ( ph /\ s e. NN0 ) -> A. k e. ( 0 ... s ) ( A .* ( k .^ X ) ) e. B )
107 106 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 )
108 fzfid 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( 0 ... s ) e. Fin )
109 1 2 98 99 107 108 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 ) ) ) )
110 nfv 
 |-  F/ k ( ph /\ s e. NN0 )
111 nfcv 
 |-  F/_ k NN0
112 111 54 nfralw 
 |-  F/ k A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. )
113 110 112 nfan 
 |-  F/ k ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) )
114 5 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> R e. Ring )
115 12 expcom 
 |-  ( k e. NN0 -> ( ph -> A e. K ) )
116 115 100 syl11 
 |-  ( ph -> ( k e. ( 0 ... s ) -> A e. K ) )
117 116 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( k e. ( 0 ... s ) -> A e. K ) )
118 117 imp 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> A e. K )
119 100 adantl 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> k e. NN0 )
120 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. ) ) )
121 114 118 119 120 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. ) ) )
122 eqeq1 
 |-  ( n = L -> ( n = k <-> L = k ) )
123 122 ifbid 
 |-  ( n = L -> if ( n = k , A , .0. ) = if ( L = k , A , .0. ) )
124 123 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. ) )
125 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> L e. NN0 )
126 6 8 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
127 5 126 syl 
 |-  ( ph -> .0. e. K )
128 127 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) /\ k e. ( 0 ... s ) ) -> .0. e. K )
129 118 128 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 )
130 121 124 125 129 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. ) )
131 113 130 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. ) ) )
132 131 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. ) ) ) )
133 breq2 
 |-  ( x = L -> ( s < x <-> s < L ) )
134 csbeq1 
 |-  ( x = L -> [_ x / k ]_ A = [_ L / k ]_ A )
135 134 eqeq1d 
 |-  ( x = L -> ( [_ x / k ]_ A = .0. <-> [_ L / k ]_ A = .0. ) )
136 133 135 imbi12d 
 |-  ( x = L -> ( ( s < x -> [_ x / k ]_ A = .0. ) <-> ( s < L -> [_ L / k ]_ A = .0. ) ) )
137 136 rspcva 
 |-  ( ( L e. NN0 /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( s < L -> [_ L / k ]_ A = .0. ) )
138 nfv 
 |-  F/ k ( ph /\ ( s e. NN0 /\ s < L ) )
139 nfcsb1v 
 |-  F/_ k [_ L / k ]_ A
140 139 nfeq1 
 |-  F/ k [_ L / k ]_ A = .0.
141 138 140 nfan 
 |-  F/ k ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. )
142 elfz2nn0 
 |-  ( k e. ( 0 ... s ) <-> ( k e. NN0 /\ s e. NN0 /\ k <_ s ) )
143 nn0re 
 |-  ( k e. NN0 -> k e. RR )
144 143 ad2antrr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> k e. RR )
145 nn0re 
 |-  ( s e. NN0 -> s e. RR )
146 145 adantl 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> s e. RR )
147 146 adantr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> s e. RR )
148 nn0re 
 |-  ( L e. NN0 -> L e. RR )
149 148 adantl 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> L e. RR )
150 lelttr 
 |-  ( ( k e. RR /\ s e. RR /\ L e. RR ) -> ( ( k <_ s /\ s < L ) -> k < L ) )
151 144 147 149 150 syl3anc 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( ( k <_ s /\ s < L ) -> k < L ) )
152 animorr 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> ( L < k \/ k < L ) )
153 df-ne 
 |-  ( L =/= k <-> -. L = k )
154 143 adantr 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> k e. RR )
155 lttri2 
 |-  ( ( L e. RR /\ k e. RR ) -> ( L =/= k <-> ( L < k \/ k < L ) ) )
156 148 154 155 syl2anr 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( L =/= k <-> ( L < k \/ k < L ) ) )
157 156 adantr 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> ( L =/= k <-> ( L < k \/ k < L ) ) )
158 153 157 bitr3id 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> ( -. L = k <-> ( L < k \/ k < L ) ) )
159 152 158 mpbird 
 |-  ( ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) /\ k < L ) -> -. L = k )
160 159 ex 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( k < L -> -. L = k ) )
161 151 160 syld 
 |-  ( ( ( k e. NN0 /\ s e. NN0 ) /\ L e. NN0 ) -> ( ( k <_ s /\ s < L ) -> -. L = k ) )
162 161 exp4b 
 |-  ( ( k e. NN0 /\ s e. NN0 ) -> ( L e. NN0 -> ( k <_ s -> ( s < L -> -. L = k ) ) ) )
163 162 expimpd 
 |-  ( k e. NN0 -> ( ( s e. NN0 /\ L e. NN0 ) -> ( k <_ s -> ( s < L -> -. L = k ) ) ) )
164 163 com23 
 |-  ( k e. NN0 -> ( k <_ s -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) ) )
165 164 imp 
 |-  ( ( k e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) )
166 165 3adant2 
 |-  ( ( k e. NN0 /\ s e. NN0 /\ k <_ s ) -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) )
167 142 166 sylbi 
 |-  ( k e. ( 0 ... s ) -> ( ( s e. NN0 /\ L e. NN0 ) -> ( s < L -> -. L = k ) ) )
168 167 expd 
 |-  ( k e. ( 0 ... s ) -> ( s e. NN0 -> ( L e. NN0 -> ( s < L -> -. L = k ) ) ) )
169 11 168 syl7 
 |-  ( k e. ( 0 ... s ) -> ( s e. NN0 -> ( ph -> ( s < L -> -. L = k ) ) ) )
170 169 com12 
 |-  ( s e. NN0 -> ( k e. ( 0 ... s ) -> ( ph -> ( s < L -> -. L = k ) ) ) )
171 170 com24 
 |-  ( s e. NN0 -> ( s < L -> ( ph -> ( k e. ( 0 ... s ) -> -. L = k ) ) ) )
172 171 imp 
 |-  ( ( s e. NN0 /\ s < L ) -> ( ph -> ( k e. ( 0 ... s ) -> -. L = k ) ) )
173 172 impcom 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> ( k e. ( 0 ... s ) -> -. L = k ) )
174 173 adantr 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( k e. ( 0 ... s ) -> -. L = k ) )
175 174 imp 
 |-  ( ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) /\ k e. ( 0 ... s ) ) -> -. L = k )
176 175 iffalsed 
 |-  ( ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) /\ k e. ( 0 ... s ) ) -> if ( L = k , A , .0. ) = .0. )
177 141 176 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. ) )
178 177 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. ) ) )
179 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
180 5 179 syl 
 |-  ( ph -> R e. Mnd )
181 180 adantr 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> R e. Mnd )
182 ovex 
 |-  ( 0 ... s ) e. _V
183 8 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... s ) e. _V ) -> ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) = .0. )
184 181 182 183 sylancl 
 |-  ( ( ph /\ ( s e. NN0 /\ s < L ) ) -> ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) = .0. )
185 184 adantr 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> ( R gsum ( k e. ( 0 ... s ) |-> .0. ) ) = .0. )
186 id 
 |-  ( [_ L / k ]_ A = .0. -> [_ L / k ]_ A = .0. )
187 186 eqcomd 
 |-  ( [_ L / k ]_ A = .0. -> .0. = [_ L / k ]_ A )
188 187 adantl 
 |-  ( ( ( ph /\ ( s e. NN0 /\ s < L ) ) /\ [_ L / k ]_ A = .0. ) -> .0. = [_ L / k ]_ A )
189 178 185 188 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 )
190 189 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 ) )
191 190 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 ) ) )
192 191 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 ) ) )
193 192 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 ) ) ) )
194 193 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 ) ) ) )
195 137 194 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 ) ) ) )
196 195 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 ) ) ) ) )
197 196 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 ) ) ) ) )
198 11 197 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 ) ) ) )
199 198 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 ) )
200 199 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 ) )
201 pm3.2 
 |-  ( ( ph /\ s e. NN0 ) -> ( -. s < L -> ( ( ph /\ s e. NN0 ) /\ -. s < L ) ) )
202 201 adantr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> [_ x / k ]_ A = .0. ) ) -> ( -. s < L -> ( ( ph /\ s e. NN0 ) /\ -. s < L ) ) )
203 180 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> R e. Mnd )
204 182 a1i 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> ( 0 ... s ) e. _V )
205 11 nn0red 
 |-  ( ph -> L e. RR )
206 lenlt 
 |-  ( ( L e. RR /\ s e. RR ) -> ( L <_ s <-> -. s < L ) )
207 205 145 206 syl2an 
 |-  ( ( ph /\ s e. NN0 ) -> ( L <_ s <-> -. s < L ) )
208 11 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> L e. NN0 )
209 simplr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> s e. NN0 )
210 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> L <_ s )
211 elfz2nn0 
 |-  ( L e. ( 0 ... s ) <-> ( L e. NN0 /\ s e. NN0 /\ L <_ s ) )
212 208 209 210 211 syl3anbrc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ L <_ s ) -> L e. ( 0 ... s ) )
213 212 ex 
 |-  ( ( ph /\ s e. NN0 ) -> ( L <_ s -> L e. ( 0 ... s ) ) )
214 207 213 sylbird 
 |-  ( ( ph /\ s e. NN0 ) -> ( -. s < L -> L e. ( 0 ... s ) ) )
215 214 imp 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> L e. ( 0 ... s ) )
216 eqcom 
 |-  ( L = k <-> k = L )
217 ifbi 
 |-  ( ( L = k <-> k = L ) -> if ( L = k , A , .0. ) = if ( k = L , A , .0. ) )
218 216 217 ax-mp 
 |-  if ( L = k , A , .0. ) = if ( k = L , A , .0. )
219 218 mpteq2i 
 |-  ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) = ( k e. ( 0 ... s ) |-> if ( k = L , A , .0. ) )
220 12 6 eleqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> A e. ( Base ` R ) )
221 220 ex 
 |-  ( ph -> ( k e. NN0 -> A e. ( Base ` R ) ) )
222 221 adantr 
 |-  ( ( ph /\ s e. NN0 ) -> ( k e. NN0 -> A e. ( Base ` R ) ) )
223 222 100 impel 
 |-  ( ( ( ph /\ s e. NN0 ) /\ k e. ( 0 ... s ) ) -> A e. ( Base ` R ) )
224 223 ralrimiva 
 |-  ( ( ph /\ s e. NN0 ) -> A. k e. ( 0 ... s ) A e. ( Base ` R ) )
225 224 adantr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> A. k e. ( 0 ... s ) A e. ( Base ` R ) )
226 8 203 204 215 219 225 gsummpt1n0 
 |-  ( ( ( ph /\ s e. NN0 ) /\ -. s < L ) -> ( R gsum ( k e. ( 0 ... s ) |-> if ( L = k , A , .0. ) ) ) = [_ L / k ]_ A )
227 202 226 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 ) )
228 200 227 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 )
229 132 228 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 )
230 97 109 229 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 )
231 230 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 ) )
232 34 231 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 ) )
233 232 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 ) )
234 23 233 mpd 
 |-  ( ph -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ A )