MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsummoncoe1 Structured version   Unicode version

Theorem gsummoncoe1 18885
Description: A coefficient of the polynomial represented as sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019.)
Hypotheses
Ref Expression
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
Ref Expression
gsummoncoe1  |-  ( ph  ->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  [_ L  /  k ]_ A
)
Distinct variable groups:    B, k    k, K    ph, k    .* , k    k, L    P, k    R, k    .0. , k    .^ , k
Allowed substitution hints:    A( k)    X( k)

Proof of Theorem gsummoncoe1
Dummy variables  n  s  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsummonply1.f . . 3  |-  ( ph  ->  ( k  e.  NN0  |->  A ) finSupp  .0.  )
2 gsummonply1.a . . . . . . 7  |-  ( ph  ->  A. k  e.  NN0  A  e.  K )
32r19.21bi 2794 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  A  e.  K )
4 eqid 2422 . . . . . 6  |-  ( k  e.  NN0  |->  A )  =  ( k  e. 
NN0  |->  A )
53, 4fmptd 6057 . . . . 5  |-  ( ph  ->  ( k  e.  NN0  |->  A ) : NN0 --> K )
6 gsummonply1.k . . . . . . . 8  |-  K  =  ( Base `  R
)
7 fvex 5887 . . . . . . . 8  |-  ( Base `  R )  e.  _V
86, 7eqeltri 2506 . . . . . . 7  |-  K  e. 
_V
98a1i 11 . . . . . 6  |-  ( ph  ->  K  e.  _V )
10 nn0ex 10875 . . . . . 6  |-  NN0  e.  _V
11 elmapg 7489 . . . . . 6  |-  ( ( K  e.  _V  /\  NN0 
e.  _V )  ->  (
( k  e.  NN0  |->  A )  e.  ( K  ^m  NN0 )  <->  ( k  e.  NN0  |->  A ) : NN0 --> K ) )
129, 10, 11sylancl 666 . . . . 5  |-  ( ph  ->  ( ( k  e. 
NN0  |->  A )  e.  ( K  ^m  NN0 ) 
<->  ( k  e.  NN0  |->  A ) : NN0 --> K ) )
135, 12mpbird 235 . . . 4  |-  ( ph  ->  ( k  e.  NN0  |->  A )  e.  ( K  ^m  NN0 )
)
14 gsummonply1.0 . . . . 5  |-  .0.  =  ( 0g `  R )
15 fvex 5887 . . . . 5  |-  ( 0g
`  R )  e. 
_V
1614, 15eqeltri 2506 . . . 4  |-  .0.  e.  _V
17 fsuppmapnn0ub 12206 . . . 4  |-  ( ( ( 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.  )
) )
1813, 16, 17sylancl 666 . . 3  |-  ( ph  ->  ( ( k  e. 
NN0  |->  A ) finSupp  .0.  ->  E. s  e.  NN0  A. x  e.  NN0  (
s  <  x  ->  ( ( k  e.  NN0  |->  A ) `  x
)  =  .0.  )
) )
191, 18mpd 15 . 2  |-  ( ph  ->  E. s  e.  NN0  A. x  e.  NN0  (
s  <  x  ->  ( ( k  e.  NN0  |->  A ) `  x
)  =  .0.  )
)
20 simpr 462 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  x  e.  NN0 )
212ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  A. k  e.  NN0  A  e.  K
)
22 rspcsbela 3823 . . . . . . . . . 10  |-  ( ( x  e.  NN0  /\  A. k  e.  NN0  A  e.  K )  ->  [_ x  /  k ]_ A  e.  K )
2320, 21, 22syl2anc 665 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  [_ x  /  k ]_ A  e.  K )
244fvmpts 5963 . . . . . . . . 9  |-  ( ( x  e.  NN0  /\  [_ x  /  k ]_ A  e.  K )  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  [_ x  /  k ]_ A
)
2520, 23, 24syl2anc 665 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( k  e.  NN0  |->  A ) `  x
)  =  [_ x  /  k ]_ A
)
2625eqeq1d 2424 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  <->  [_ x  /  k ]_ A  =  .0.  )
)
2726imbi2d 317 . . . . . 6  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( s  <  x  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  )  <->  ( s  < 
x  ->  [_ x  / 
k ]_ A  =  .0.  ) ) )
2827biimpd 210 . . . . 5  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( s  <  x  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  )  ->  ( s  <  x  ->  [_ x  / 
k ]_ A  =  .0.  ) ) )
2928ralimdva 2833 . . . 4  |-  ( (
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.  ) ) )
30 nfv 1751 . . . . . . . . . 10  |-  F/ k ( ph  /\  s  e.  NN0 )
31 nfcv 2584 . . . . . . . . . . 11  |-  F/_ k NN0
32 nfv 1751 . . . . . . . . . . . 12  |-  F/ k  s  <  x
33 nfcsb1v 3411 . . . . . . . . . . . . 13  |-  F/_ k [_ x  /  k ]_ A
3433nfeq1 2599 . . . . . . . . . . . 12  |-  F/ k
[_ x  /  k ]_ A  =  .0.
3532, 34nfim 1976 . . . . . . . . . . 11  |-  F/ k ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
3631, 35nfral 2811 . . . . . . . . . 10  |-  F/ k A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
3730, 36nfan 1984 . . . . . . . . 9  |-  F/ k ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)
38 gsummonply1.b . . . . . . . . 9  |-  B  =  ( Base `  P
)
39 eqid 2422 . . . . . . . . 9  |-  ( 0g
`  P )  =  ( 0g `  P
)
40 gsummonply1.r . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Ring )
41 gsummonply1.p . . . . . . . . . . . 12  |-  P  =  (Poly1 `  R )
4241ply1ring 18828 . . . . . . . . . . 11  |-  ( R  e.  Ring  ->  P  e. 
Ring )
43 ringcmn 17798 . . . . . . . . . . 11  |-  ( P  e.  Ring  ->  P  e. CMnd
)
4440, 42, 433syl 18 . . . . . . . . . 10  |-  ( ph  ->  P  e. CMnd )
4544ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  P  e. CMnd )
46403ad2ant1 1026 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  R  e.  Ring )
47 simp3 1007 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  A  e.  K )
48 simp2 1006 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  k  e.  NN0 )
49 gsummonply1.x . . . . . . . . . . . . . . 15  |-  X  =  (var1 `  R )
50 gsummonply1.m . . . . . . . . . . . . . . 15  |-  .*  =  ( .s `  P )
51 eqid 2422 . . . . . . . . . . . . . . 15  |-  (mulGrp `  P )  =  (mulGrp `  P )
52 gsummonply1.e . . . . . . . . . . . . . . 15  |-  .^  =  (.g
`  (mulGrp `  P )
)
536, 41, 49, 50, 51, 52, 38ply1tmcl 18852 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Ring  /\  A  e.  K  /\  k  e.  NN0 )  ->  ( A  .*  ( k  .^  X ) )  e.  B )
5446, 47, 48, 53syl3anc 1264 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  ( A  .*  ( k  .^  X
) )  e.  B
)
55543expia 1207 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( A  e.  K  ->  ( A  .*  ( k  .^  X ) )  e.  B ) )
5655ralimdva 2833 . . . . . . . . . . 11  |-  ( ph  ->  ( A. k  e. 
NN0  A  e.  K  ->  A. k  e.  NN0  ( A  .*  (
k  .^  X )
)  e.  B ) )
572, 56mpd 15 . . . . . . . . . 10  |-  ( ph  ->  A. k  e.  NN0  ( A  .*  (
k  .^  X )
)  e.  B )
5857ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  A. k  e.  NN0  ( A  .*  (
k  .^  X )
)  e.  B )
59 simplr 760 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
s  e.  NN0 )
60 nfv 1751 . . . . . . . . . . . 12  |-  F/ x
( s  <  k  ->  [_ k  /  k ]_ A  =  .0.  )
61 breq2 4424 . . . . . . . . . . . . 13  |-  ( x  =  k  ->  (
s  <  x  <->  s  <  k ) )
62 csbeq1 3398 . . . . . . . . . . . . . 14  |-  ( x  =  k  ->  [_ x  /  k ]_ A  =  [_ k  /  k ]_ A )
6362eqeq1d 2424 . . . . . . . . . . . . 13  |-  ( x  =  k  ->  ( [_ x  /  k ]_ A  =  .0.  <->  [_ k  /  k ]_ A  =  .0.  ) )
6461, 63imbi12d 321 . . . . . . . . . . . 12  |-  ( x  =  k  ->  (
( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) 
<->  ( s  <  k  ->  [_ k  /  k ]_ A  =  .0.  ) ) )
6535, 60, 64cbvral 3051 . . . . . . . . . . 11  |-  ( A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )  <->  A. k  e.  NN0  ( s  < 
k  ->  [_ k  / 
k ]_ A  =  .0.  ) )
66 csbid 3403 . . . . . . . . . . . . . . 15  |-  [_ k  /  k ]_ A  =  A
6766eqeq1i 2429 . . . . . . . . . . . . . 14  |-  ( [_ k  /  k ]_ A  =  .0.  <->  A  =  .0.  )
68 oveq1 6308 . . . . . . . . . . . . . . . 16  |-  ( A  =  .0.  ->  ( A  .*  ( k  .^  X ) )  =  (  .0.  .*  (
k  .^  X )
) )
6941ply1sca 18833 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  Ring  ->  R  =  (Scalar `  P )
)
7040, 69syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  R  =  (Scalar `  P ) )
7170fveq2d 5881 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0g `  R
)  =  ( 0g
`  (Scalar `  P )
) )
7214, 71syl5eq 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  .0.  =  ( 0g
`  (Scalar `  P )
) )
7372ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  .0.  =  ( 0g `  (Scalar `  P ) ) )
7473oveq1d 6316 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (  .0.  .*  ( k  .^  X ) )  =  ( ( 0g `  (Scalar `  P ) )  .*  ( k  .^  X ) ) )
7541ply1lmod 18832 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  Ring  ->  P  e. 
LMod )
7640, 75syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  P  e.  LMod )
7776ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  P  e.  LMod )
7851ringmgp 17773 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  Ring  ->  (mulGrp `  P )  e.  Mnd )
7940, 42, 783syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  (mulGrp `  P )  e.  Mnd )
8079ad2antrr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (mulGrp `  P )  e.  Mnd )
81 simpr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
82 eqid 2422 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Base `  P )  =  (
Base `  P )
8349, 41, 82vr1cl 18797 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  Ring  ->  X  e.  ( Base `  P
) )
8440, 83syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  X  e.  ( Base `  P ) )
8584ad2antrr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  X  e.  ( Base `  P
) )
8651, 82mgpbas 17716 . . . . . . . . . . . . . . . . . . . 20  |-  ( Base `  P )  =  (
Base `  (mulGrp `  P
) )
8786, 52mulgnn0cl 16761 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (mulGrp `  P )  e.  Mnd  /\  k  e. 
NN0  /\  X  e.  ( Base `  P )
)  ->  ( k  .^  X )  e.  (
Base `  P )
)
8880, 81, 85, 87syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (
k  .^  X )  e.  ( Base `  P
) )
89 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  (Scalar `  P )  =  (Scalar `  P )
90 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  ( 0g
`  (Scalar `  P )
)  =  ( 0g
`  (Scalar `  P )
)
9182, 89, 50, 90, 39lmod0vs 18111 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e.  LMod  /\  (
k  .^  X )  e.  ( Base `  P
) )  ->  (
( 0g `  (Scalar `  P ) )  .*  ( k  .^  X
) )  =  ( 0g `  P ) )
9277, 88, 91syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (
( 0g `  (Scalar `  P ) )  .*  ( k  .^  X
) )  =  ( 0g `  P ) )
9374, 92eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (  .0.  .*  ( k  .^  X ) )  =  ( 0g `  P
) )
9468, 93sylan9eqr 2485 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  /\  A  =  .0.  )  ->  ( A  .*  (
k  .^  X )
)  =  ( 0g
`  P ) )
9594ex 435 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ( A  =  .0.  ->  ( A  .*  ( k 
.^  X ) )  =  ( 0g `  P ) ) )
9667, 95syl5bi 220 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ( [_ k  /  k ]_ A  =  .0.  ->  ( A  .*  (
k  .^  X )
)  =  ( 0g
`  P ) ) )
9796imim2d 54 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (
( s  <  k  ->  [_ k  /  k ]_ A  =  .0.  )  ->  ( s  < 
k  ->  ( A  .*  ( k  .^  X
) )  =  ( 0g `  P ) ) ) )
9897ralimdva 2833 . . . . . . . . . . 11  |-  ( (
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 ) ) ) )
9965, 98syl5bi 220 . . . . . . . . . 10  |-  ( (
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 ) ) ) )
10099imp 430 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
10137, 38, 39, 45, 58, 59, 100gsummptnn0fz 17602 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( P  gsumg  ( k  e.  NN0  |->  ( A  .*  (
k  .^  X )
) ) )  =  ( P  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( A  .*  (
k  .^  X )
) ) ) )
102101fveq2d 5881 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
(coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) )  =  (coe1 `  ( P  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( A  .*  (
k  .^  X )
) ) ) ) )
103102fveq1d 5879 . . . . . 6  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  ( (coe1 `  ( P  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( A  .*  (
k  .^  X )
) ) ) ) `
 L ) )
10440ad2antrr 730 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  R  e.  Ring )
105 gsummonply1.l . . . . . . . 8  |-  ( ph  ->  L  e.  NN0 )
106105ad2antrr 730 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  L  e.  NN0 )
107 elfznn0 11887 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... s )  ->  k  e.  NN0 )
108 simpll 758 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ph )
1093adantlr 719 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  A  e.  K )
110108, 81, 1093jca 1185 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ( ph  /\  k  e.  NN0  /\  A  e.  K ) )
111107, 110sylan2 476 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  ( 0 ... s
) )  ->  ( ph  /\  k  e.  NN0  /\  A  e.  K ) )
112111, 54syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  ( 0 ... s
) )  ->  ( A  .*  ( k  .^  X ) )  e.  B )
113112ralrimiva 2839 . . . . . . . 8  |-  ( (
ph  /\  s  e.  NN0 )  ->  A. k  e.  ( 0 ... s
) ( A  .*  ( k  .^  X
) )  e.  B
)
114113adantr 466 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  A. k  e.  (
0 ... s ) ( A  .*  ( k 
.^  X ) )  e.  B )
115 fzfid 12185 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( 0 ... s
)  e.  Fin )
11641, 38, 104, 106, 114, 115coe1fzgsumd 18883 . . . . . 6  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( (coe1 `  ( P  gsumg  ( k  e.  ( 0 ... s )  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  ( R 
gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( A  .*  ( k  .^  X
) ) ) `  L ) ) ) )
11740ad3antrrr 734 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  R  e.  Ring )
1183expcom 436 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  ( ph  ->  A  e.  K ) )
119107, 118syl 17 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... s )  ->  ( ph  ->  A  e.  K
) )
120119com12 32 . . . . . . . . . . . . 13  |-  ( ph  ->  ( k  e.  ( 0 ... s )  ->  A  e.  K
) )
121120ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( k  e.  ( 0 ... s )  ->  A  e.  K
) )
122121imp 430 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  A  e.  K )
123107adantl 467 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  k  e.  NN0 )
12414, 6, 41, 49, 50, 51, 52coe1tm 18853 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  A  e.  K  /\  k  e.  NN0 )  ->  (coe1 `  ( A  .*  (
k  .^  X )
) )  =  ( n  e.  NN0  |->  if ( n  =  k ,  A ,  .0.  )
) )
125117, 122, 123, 124syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ( 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.  )
) )
126 eqeq1 2426 . . . . . . . . . . . 12  |-  ( n  =  L  ->  (
n  =  k  <->  L  =  k ) )
127126ifbid 3931 . . . . . . . . . . 11  |-  ( n  =  L  ->  if ( n  =  k ,  A ,  .0.  )  =  if ( L  =  k ,  A ,  .0.  ) )
128127adantl 467 . . . . . . . . . 10  |-  ( ( ( ( ( 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.  ) )
129105ad3antrrr 734 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  L  e.  NN0 )
1306, 14ring0cl 17789 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  .0.  e.  K )
13140, 130syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  .0.  e.  K )
132131ad3antrrr 734 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  .0.  e.  K )
133122, 132ifcld 3952 . . . . . . . . . 10  |-  ( ( ( ( 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 )
134125, 128, 129, 133fvmptd 5966 . . . . . . . . 9  |-  ( ( ( ( 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.  ) )
13537, 134mpteq2da 4506 . . . . . . . 8  |-  ( ( ( 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.  ) ) )
136135oveq2d 6317 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( A  .*  ( k  .^  X
) ) ) `  L ) ) )  =  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  )
) ) )
137 breq2 4424 . . . . . . . . . . . . . . . 16  |-  ( x  =  L  ->  (
s  <  x  <->  s  <  L ) )
138 csbeq1 3398 . . . . . . . . . . . . . . . . 17  |-  ( x  =  L  ->  [_ x  /  k ]_ A  =  [_ L  /  k ]_ A )
139138eqeq1d 2424 . . . . . . . . . . . . . . . 16  |-  ( x  =  L  ->  ( [_ x  /  k ]_ A  =  .0.  <->  [_ L  /  k ]_ A  =  .0.  ) )
140137, 139imbi12d 321 . . . . . . . . . . . . . . 15  |-  ( x  =  L  ->  (
( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) 
<->  ( s  <  L  ->  [_ L  /  k ]_ A  =  .0.  ) ) )
141140rspcva 3180 . . . . . . . . . . . . . 14  |-  ( ( L  e.  NN0  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  ->  ( s  <  L  ->  [_ L  / 
k ]_ A  =  .0.  ) )
142 nfv 1751 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )
143 nfcsb1v 3411 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ k [_ L  /  k ]_ A
144143nfeq1 2599 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k
[_ L  /  k ]_ A  =  .0.
145142, 144nfan 1984 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ k ( ( ph  /\  ( s  e.  NN0  /\  s  <  L ) )  /\  [_ L  /  k ]_ A  =  .0.  )
146 elfz2nn0 11885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ( 0 ... s )  <->  ( k  e.  NN0  /\  s  e. 
NN0  /\  k  <_  s ) )
147 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( k  e.  NN0  ->  k  e.  RR )
148147ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  k  e.  RR )
149 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( s  e.  NN0  ->  s  e.  RR )
150149adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
s  e.  RR )
151150adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  s  e.  RR )
152 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( L  e.  NN0  ->  L  e.  RR )
153152adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  L  e.  RR )
154 lelttr 9724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( k  e.  RR  /\  s  e.  RR  /\  L  e.  RR )  ->  (
( k  <_  s  /\  s  <  L )  ->  k  <  L
) )
155148, 151, 153, 154syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  ( ( k  <_  s  /\  s  <  L )  ->  k  <  L ) )
156 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  k  <  L )
157156olcd 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  ( L  <  k  \/  k  <  L ) )
158 df-ne 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( L  =/=  k  <->  -.  L  =  k )
159147adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
k  e.  RR )
160 lttri2 9716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( L  e.  RR  /\  k  e.  RR )  ->  ( L  =/=  k  <->  ( L  <  k  \/  k  <  L ) ) )
161152, 159, 160syl2anr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  ( L  =/=  k  <->  ( L  < 
k  \/  k  < 
L ) ) )
162161adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  ( L  =/=  k  <->  ( L  <  k  \/  k  < 
L ) ) )
163158, 162syl5bbr 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  ( -.  L  =  k  <->  ( L  <  k  \/  k  <  L ) ) )
164157, 163mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  -.  L  =  k )
165164ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  ( k  < 
L  ->  -.  L  =  k ) )
166155, 165syld 45 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  ( ( k  <_  s  /\  s  <  L )  ->  -.  L  =  k )
)
167166exp4b 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
( L  e.  NN0  ->  ( k  <_  s  ->  ( s  <  L  ->  -.  L  =  k ) ) ) )
168167expimpd 606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN0  ->  ( ( s  e.  NN0  /\  L  e.  NN0 )  -> 
( k  <_  s  ->  ( s  <  L  ->  -.  L  =  k ) ) ) )
169168com23 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  NN0  ->  ( k  <_  s  ->  (
( s  e.  NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) ) )
170169imp 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  NN0  /\  k  <_  s )  -> 
( ( s  e. 
NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) )
1711703adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( k  e.  NN0  /\  s  e.  NN0  /\  k  <_  s )  ->  (
( s  e.  NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) )
172146, 171sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ( 0 ... s )  ->  (
( s  e.  NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) )
173172expd 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  e.  ( 0 ... s )  ->  (
s  e.  NN0  ->  ( L  e.  NN0  ->  ( s  <  L  ->  -.  L  =  k
) ) ) )
174105, 173syl7 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  ( 0 ... s )  ->  (
s  e.  NN0  ->  (
ph  ->  ( s  < 
L  ->  -.  L  =  k ) ) ) )
175174com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  NN0  ->  ( k  e.  ( 0 ... s )  ->  ( ph  ->  ( s  < 
L  ->  -.  L  =  k ) ) ) )
176175com24 90 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  NN0  ->  ( s  <  L  ->  ( ph  ->  ( k  e.  ( 0 ... s
)  ->  -.  L  =  k ) ) ) )
177176imp 430 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  NN0  /\  s  <  L )  -> 
( ph  ->  ( k  e.  ( 0 ... s )  ->  -.  L  =  k )
) )
178177impcom 431 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  -> 
( k  e.  ( 0 ... s )  ->  -.  L  =  k ) )
179178adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( k  e.  ( 0 ... s
)  ->  -.  L  =  k ) )
180179imp 430 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( s  e.  NN0  /\  s  <  L ) )  /\  [_ L  /  k ]_ A  =  .0.  )  /\  k  e.  ( 0 ... s
) )  ->  -.  L  =  k )
181180iffalsed 3920 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( s  e.  NN0  /\  s  <  L ) )  /\  [_ L  /  k ]_ A  =  .0.  )  /\  k  e.  ( 0 ... s
) )  ->  if ( L  =  k ,  A ,  .0.  )  =  .0.  )
182145, 181mpteq2da 4506 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( k  e.  ( 0 ... s
)  |->  if ( L  =  k ,  A ,  .0.  ) )  =  ( k  e.  ( 0 ... s ) 
|->  .0.  ) )
183182oveq2d 6317 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  =  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  .0.  ) ) )
184 ringmnd 17776 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
18540, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  R  e.  Mnd )
186185adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  ->  R  e.  Mnd )
187 ovex 6329 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 ... s )  e. 
_V
18814gsumz 16608 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  Mnd  /\  ( 0 ... s
)  e.  _V )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  .0.  ) )  =  .0.  )
189186, 187, 188sylancl 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  .0.  ) )  =  .0.  )
190189adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  .0.  ) )  =  .0.  )
191 id 23 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( [_ L  /  k ]_ A  =  .0.  ->  [_ L  / 
k ]_ A  =  .0.  )
192191eqcomd 2430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( [_ L  /  k ]_ A  =  .0.  ->  .0.  =  [_ L  /  k ]_ A )
193192adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  .0.  =  [_ L  /  k ]_ A )
194183, 190, 1933eqtrd 2467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A )
195194ex 435 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  -> 
( [_ L  /  k ]_ A  =  .0.  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) )
196195expr 618 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( s  <  L  ->  ( [_ L  /  k ]_ A  =  .0.  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) )
197196a2d 29 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( (
s  <  L  ->  [_ L  /  k ]_ A  =  .0.  )  ->  ( s  <  L  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) )
198197ex 435 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( s  e.  NN0  ->  ( ( s  < 
L  ->  [_ L  / 
k ]_ A  =  .0.  )  ->  ( s  <  L  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) ) )
199198com13 83 . . . . . . . . . . . . . 14  |-  ( ( s  <  L  ->  [_ L  /  k ]_ A  =  .0.  )  ->  ( s  e. 
NN0  ->  ( ph  ->  ( s  <  L  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) ) )
200141, 199syl 17 . . . . . . . . . . . . 13  |-  ( ( L  e.  NN0  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  ->  ( s  e.  NN0  ->  ( ph  ->  ( s  <  L  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) ) )
201200ex 435 . . . . . . . . . . . 12  |-  ( L  e.  NN0  ->  ( A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )  ->  (
s  e.  NN0  ->  (
ph  ->  ( s  < 
L  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) ) ) )
202201com24 90 . . . . . . . . . . 11  |-  ( L  e.  NN0  ->  ( ph  ->  ( s  e.  NN0  ->  ( A. x  e. 
NN0  ( s  < 
x  ->  [_ x  / 
k ]_ A  =  .0.  )  ->  ( s  <  L  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) ) ) )
203105, 202mpcom 37 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  NN0  ->  ( A. x  e. 
NN0  ( s  < 
x  ->  [_ x  / 
k ]_ A  =  .0.  )  ->  ( s  <  L  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) ) ) )
204203imp31 433 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( s  <  L  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) )
205204com12 32 . . . . . . . 8  |-  ( s  <  L  ->  (
( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) )
206 pm3.2 448 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( -.  s  <  L  ->  (
( ph  /\  s  e.  NN0 )  /\  -.  s  <  L ) ) )
207206adantr 466 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( -.  s  < 
L  ->  ( ( ph  /\  s  e.  NN0 )  /\  -.  s  < 
L ) ) )
208185ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  ->  R  e.  Mnd )
209187a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  -> 
( 0 ... s
)  e.  _V )
210105nn0red 10926 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  RR )
211 lenlt 9712 . . . . . . . . . . . . 13  |-  ( ( L  e.  RR  /\  s  e.  RR )  ->  ( L  <_  s  <->  -.  s  <  L ) )
212210, 149, 211syl2an 479 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( L  <_  s  <->  -.  s  <  L ) )
213105ad2antrr 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  L  e.  NN0 )
214 simplr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  s  e.  NN0 )
215 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  L  <_  s )
216 elfz2nn0 11885 . . . . . . . . . . . . . 14  |-  ( L  e.  ( 0 ... s )  <->  ( L  e.  NN0  /\  s  e. 
NN0  /\  L  <_  s ) )
217213, 214, 215, 216syl3anbrc 1189 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  L  e.  ( 0 ... s
) )
218217ex 435 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( L  <_  s  ->  L  e.  ( 0 ... s
) ) )
219212, 218sylbird 238 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( -.  s  <  L  ->  L  e.  ( 0 ... s
) ) )
220219imp 430 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  ->  L  e.  ( 0 ... s ) )
221 eqcom 2431 . . . . . . . . . . . 12  |-  ( L  =  k  <->  k  =  L )
222 ifbi 3930 . . . . . . . . . . . 12  |-  ( ( L  =  k  <->  k  =  L )  ->  if ( L  =  k ,  A ,  .0.  )  =  if ( k  =  L ,  A ,  .0.  ) )
223221, 222ax-mp 5 . . . . . . . . . . 11  |-  if ( L  =  k ,  A ,  .0.  )  =  if ( k  =  L ,  A ,  .0.  )
224223mpteq2i 4504 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  )
)  =  ( k  e.  ( 0 ... s )  |->  if ( k  =  L ,  A ,  .0.  )
)
2253, 6syl6eleq 2520 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN0 )  ->  A  e.  ( Base `  R )
)
226225ex 435 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( k  e.  NN0  ->  A  e.  ( Base `  R ) ) )
227226adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( k  e.  NN0  ->  A  e.  ( Base `  R )
) )
228107, 227syl5com 31 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... s )  ->  (
( ph  /\  s  e.  NN0 )  ->  A  e.  ( Base `  R
) ) )
229228impcom 431 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  ( 0 ... s
) )  ->  A  e.  ( Base `  R
) )
230229ralrimiva 2839 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  NN0 )  ->  A. k  e.  ( 0 ... s
) A  e.  (
Base `  R )
)
231230adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  ->  A. k  e.  (
0 ... s ) A  e.  ( Base `  R
) )
23214, 208, 209, 220, 224, 231gsummpt1n0 17584 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A )
233207, 232syl6com 36 . . . . . . . 8  |-  ( -.  s  <  L  -> 
( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A ) )
234205, 233pm2.61i 167 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  if ( L  =  k ,  A ,  .0.  ) ) )  = 
[_ L  /  k ]_ A )
235136, 234eqtrd 2463 . . . . . 6  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  ( (coe1 `  ( A  .*  ( k  .^  X
) ) ) `  L ) ) )  =  [_ L  / 
k ]_ A )
236103, 116, 2353eqtrd 2467 . . . . 5  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  [_ L  /  k ]_ A
)
237236ex 435 . . . 4  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )  ->  (
(coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  [_ L  /  k ]_ A
) )
23829, 237syld 45 . . 3  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( A. x  e.  NN0  ( s  <  x  ->  (
( k  e.  NN0  |->  A ) `  x
)  =  .0.  )  ->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  [_ L  /  k ]_ A
) )
239238rexlimdva 2917 . 2  |-  ( ph  ->  ( E. s  e. 
NN0  A. x  e.  NN0  ( s  <  x  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  )  ->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  (
k  .^  X )
) ) ) ) `
 L )  = 
[_ L  /  k ]_ A ) )
24019, 239mpd 15 1  |-  ( ph  ->  ( (coe1 `  ( P  gsumg  ( k  e.  NN0  |->  ( A  .*  ( k  .^  X ) ) ) ) ) `  L
)  =  [_ L  /  k ]_ A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868    =/= wne 2618   A.wral 2775   E.wrex 2776   _Vcvv 3081   [_csb 3395   ifcif 3909   class class class wbr 4420    |-> cmpt 4479   -->wf 5593   ` cfv 5597  (class class class)co 6301    ^m cmap 7476   finSupp cfsupp 7885   RRcr 9538   0cc0 9539    < clt 9675    <_ cle 9676   NN0cn0 10869   ...cfz 11784   Basecbs 15108  Scalarcsca 15180   .scvsca 15181   0gc0g 15325    gsumg cgsu 15326   Mndcmnd 16522  .gcmg 16659  CMndccmn 17417  mulGrpcmgp 17710   Ringcrg 17767   LModclmod 18078  var1cv1 18756  Poly1cpl1 18757  coe1cco1 18758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-ofr 6542  df-om 6703  df-1st 6803  df-2nd 6804  df-supp 6922  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-ixp 7527  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fsupp 7886  df-oi 8027  df-card 8374  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11785  df-fzo 11916  df-seq 12213  df-hash 12515  df-struct 15110  df-ndx 15111  df-slot 15112  df-base 15113  df-sets 15114  df-ress 15115  df-plusg 15190  df-mulr 15191  df-sca 15193  df-vsca 15194  df-tset 15196  df-ple 15197  df-0g 15327  df-gsum 15328  df-mre 15479  df-mrc 15480  df-acs 15482  df-mgm 16475  df-sgrp 16514  df-mnd 16524  df-mhm 16569  df-submnd 16570  df-grp 16660  df-minusg 16661  df-sbg 16662  df-mulg 16663  df-subg 16801  df-ghm 16868  df-cntz 16958  df-cmn 17419  df-abl 17420  df-mgp 17711  df-ur 17723  df-ring 17769  df-subrg 17993  df-lmod 18080  df-lss 18143  df-psr 18567  df-mvr 18568  df-mpl 18569  df-opsr 18571  df-psr1 18760  df-vr1 18761  df-ply1 18762  df-coe1 18763
This theorem is referenced by:  gsumply1eq  18886  pm2mpf1lem  19804  pm2mpcoe1  19810  pm2mpmhmlem2  19829  cayleyhamilton1  19902  ply1mulgsum  39455
  Copyright terms: Public domain W3C validator