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

Theorem gsummoncoe1 18953
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 2769 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  A  e.  K )
4 eqid 2462 . . . . . 6  |-  ( k  e.  NN0  |->  A )  =  ( k  e. 
NN0  |->  A )
53, 4fmptd 6074 . . . . 5  |-  ( ph  ->  ( k  e.  NN0  |->  A ) : NN0 --> K )
6 gsummonply1.k . . . . . . . 8  |-  K  =  ( Base `  R
)
7 fvex 5902 . . . . . . . 8  |-  ( Base `  R )  e.  _V
86, 7eqeltri 2536 . . . . . . 7  |-  K  e. 
_V
98a1i 11 . . . . . 6  |-  ( ph  ->  K  e.  _V )
10 nn0ex 10909 . . . . . 6  |-  NN0  e.  _V
11 elmapg 7516 . . . . . 6  |-  ( ( K  e.  _V  /\  NN0 
e.  _V )  ->  (
( k  e.  NN0  |->  A )  e.  ( K  ^m  NN0 )  <->  ( k  e.  NN0  |->  A ) : NN0 --> K ) )
129, 10, 11sylancl 673 . . . . 5  |-  ( ph  ->  ( ( k  e. 
NN0  |->  A )  e.  ( K  ^m  NN0 ) 
<->  ( k  e.  NN0  |->  A ) : NN0 --> K ) )
135, 12mpbird 240 . . . 4  |-  ( ph  ->  ( k  e.  NN0  |->  A )  e.  ( K  ^m  NN0 )
)
14 gsummonply1.0 . . . . 5  |-  .0.  =  ( 0g `  R )
15 fvex 5902 . . . . 5  |-  ( 0g
`  R )  e. 
_V
1614, 15eqeltri 2536 . . . 4  |-  .0.  e.  _V
17 fsuppmapnn0ub 12245 . . . 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 673 . . 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 467 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  x  e.  NN0 )
212ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  A. k  e.  NN0  A  e.  K
)
22 rspcsbela 3807 . . . . . . . . . 10  |-  ( ( x  e.  NN0  /\  A. k  e.  NN0  A  e.  K )  ->  [_ x  /  k ]_ A  e.  K )
2320, 21, 22syl2anc 671 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  [_ x  /  k ]_ A  e.  K )
244fvmpts 5979 . . . . . . . . 9  |-  ( ( x  e.  NN0  /\  [_ x  /  k ]_ A  e.  K )  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  [_ x  /  k ]_ A
)
2520, 23, 24syl2anc 671 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( k  e.  NN0  |->  A ) `  x
)  =  [_ x  /  k ]_ A
)
2625eqeq1d 2464 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  <->  [_ x  /  k ]_ A  =  .0.  )
)
2726imbi2d 322 . . . . . 6  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( s  <  x  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  )  <->  ( s  < 
x  ->  [_ x  / 
k ]_ A  =  .0.  ) ) )
2827biimpd 212 . . . . 5  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  x  e.  NN0 )  ->  (
( s  <  x  ->  ( ( k  e. 
NN0  |->  A ) `  x )  =  .0.  )  ->  ( s  <  x  ->  [_ x  / 
k ]_ A  =  .0.  ) ) )
2928ralimdva 2808 . . . 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 1772 . . . . . . . . . 10  |-  F/ k ( ph  /\  s  e.  NN0 )
31 nfcv 2603 . . . . . . . . . . 11  |-  F/_ k NN0
32 nfv 1772 . . . . . . . . . . . 12  |-  F/ k  s  <  x
33 nfcsb1v 3391 . . . . . . . . . . . . 13  |-  F/_ k [_ x  /  k ]_ A
3433nfeq1 2616 . . . . . . . . . . . 12  |-  F/ k
[_ x  /  k ]_ A  =  .0.
3532, 34nfim 2014 . . . . . . . . . . 11  |-  F/ k ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
3631, 35nfral 2786 . . . . . . . . . 10  |-  F/ k A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
3730, 36nfan 2022 . . . . . . . . 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 2462 . . . . . . . . 9  |-  ( 0g
`  P )  =  ( 0g `  P
)
40 gsummonply1.r . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Ring )
41 gsummonply1.p . . . . . . . . . . . 12  |-  P  =  (Poly1 `  R )
4241ply1ring 18896 . . . . . . . . . . 11  |-  ( R  e.  Ring  ->  P  e. 
Ring )
43 ringcmn 17866 . . . . . . . . . . 11  |-  ( P  e.  Ring  ->  P  e. CMnd
)
4440, 42, 433syl 18 . . . . . . . . . 10  |-  ( ph  ->  P  e. CMnd )
4544ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  P  e. CMnd )
46403ad2ant1 1035 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  R  e.  Ring )
47 simp3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  A  e.  K )
48 simp2 1015 . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . 15  |-  (mulGrp `  P )  =  (mulGrp `  P )
52 gsummonply1.e . . . . . . . . . . . . . . 15  |-  .^  =  (.g
`  (mulGrp `  P )
)
536, 41, 49, 50, 51, 52, 38ply1tmcl 18920 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Ring  /\  A  e.  K  /\  k  e.  NN0 )  ->  ( A  .*  ( k  .^  X ) )  e.  B )
5446, 47, 48, 53syl3anc 1276 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 
/\  A  e.  K
)  ->  ( A  .*  ( k  .^  X
) )  e.  B
)
55543expia 1217 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( A  e.  K  ->  ( A  .*  ( k  .^  X ) )  e.  B ) )
5655ralimdva 2808 . . . . . . . . . . 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 737 . . . . . . . . 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 767 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
s  e.  NN0 )
60 nfv 1772 . . . . . . . . . . . 12  |-  F/ x
( s  <  k  ->  [_ k  /  k ]_ A  =  .0.  )
61 breq2 4422 . . . . . . . . . . . . 13  |-  ( x  =  k  ->  (
s  <  x  <->  s  <  k ) )
62 csbeq1 3378 . . . . . . . . . . . . . 14  |-  ( x  =  k  ->  [_ x  /  k ]_ A  =  [_ k  /  k ]_ A )
6362eqeq1d 2464 . . . . . . . . . . . . 13  |-  ( x  =  k  ->  ( [_ x  /  k ]_ A  =  .0.  <->  [_ k  /  k ]_ A  =  .0.  ) )
6461, 63imbi12d 326 . . . . . . . . . . . 12  |-  ( x  =  k  ->  (
( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) 
<->  ( s  <  k  ->  [_ k  /  k ]_ A  =  .0.  ) ) )
6535, 60, 64cbvral 3027 . . . . . . . . . . 11  |-  ( A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )  <->  A. k  e.  NN0  ( s  < 
k  ->  [_ k  / 
k ]_ A  =  .0.  ) )
66 csbid 3383 . . . . . . . . . . . . . . 15  |-  [_ k  /  k ]_ A  =  A
6766eqeq1i 2467 . . . . . . . . . . . . . 14  |-  ( [_ k  /  k ]_ A  =  .0.  <->  A  =  .0.  )
68 oveq1 6327 . . . . . . . . . . . . . . . 16  |-  ( A  =  .0.  ->  ( A  .*  ( k  .^  X ) )  =  (  .0.  .*  (
k  .^  X )
) )
6941ply1sca 18901 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  Ring  ->  R  =  (Scalar `  P )
)
7040, 69syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  R  =  (Scalar `  P ) )
7170fveq2d 5896 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0g `  R
)  =  ( 0g
`  (Scalar `  P )
) )
7214, 71syl5eq 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  .0.  =  ( 0g
`  (Scalar `  P )
) )
7372ad2antrr 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  .0.  =  ( 0g `  (Scalar `  P ) ) )
7473oveq1d 6335 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (  .0.  .*  ( k  .^  X ) )  =  ( ( 0g `  (Scalar `  P ) )  .*  ( k  .^  X ) ) )
7541ply1lmod 18900 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  Ring  ->  P  e. 
LMod )
7640, 75syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  P  e.  LMod )
7776ad2antrr 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  P  e.  LMod )
7851ringmgp 17841 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  Ring  ->  (mulGrp `  P )  e.  Mnd )
7940, 42, 783syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  (mulGrp `  P )  e.  Mnd )
8079ad2antrr 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (mulGrp `  P )  e.  Mnd )
81 simpr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
82 eqid 2462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Base `  P )  =  (
Base `  P )
8349, 41, 82vr1cl 18865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  Ring  ->  X  e.  ( Base `  P
) )
8440, 83syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  X  e.  ( Base `  P ) )
8584ad2antrr 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  X  e.  ( Base `  P
) )
8651, 82mgpbas 17784 . . . . . . . . . . . . . . . . . . . 20  |-  ( Base `  P )  =  (
Base `  (mulGrp `  P
) )
8786, 52mulgnn0cl 16829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (mulGrp `  P )  e.  Mnd  /\  k  e. 
NN0  /\  X  e.  ( Base `  P )
)  ->  ( k  .^  X )  e.  (
Base `  P )
)
8880, 81, 85, 87syl3anc 1276 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (
k  .^  X )  e.  ( Base `  P
) )
89 eqid 2462 . . . . . . . . . . . . . . . . . . 19  |-  (Scalar `  P )  =  (Scalar `  P )
90 eqid 2462 . . . . . . . . . . . . . . . . . . 19  |-  ( 0g
`  (Scalar `  P )
)  =  ( 0g
`  (Scalar `  P )
)
9182, 89, 50, 90, 39lmod0vs 18179 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e.  LMod  /\  (
k  .^  X )  e.  ( Base `  P
) )  ->  (
( 0g `  (Scalar `  P ) )  .*  ( k  .^  X
) )  =  ( 0g `  P ) )
9277, 88, 91syl2anc 671 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (
( 0g `  (Scalar `  P ) )  .*  ( k  .^  X
) )  =  ( 0g `  P ) )
9374, 92eqtrd 2496 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  (  .0.  .*  ( k  .^  X ) )  =  ( 0g `  P
) )
9468, 93sylan9eqr 2518 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  /\  A  =  .0.  )  ->  ( A  .*  (
k  .^  X )
)  =  ( 0g
`  P ) )
9594ex 440 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ( A  =  .0.  ->  ( A  .*  ( k 
.^  X ) )  =  ( 0g `  P ) ) )
9667, 95syl5bi 225 . . . . . . . . . . . . 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 2808 . . . . . . . . . . 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 225 . . . . . . . . . 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 435 . . . . . . . . 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 17670 . . . . . . . 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 5896 . . . . . . 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 5894 . . . . . 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 737 . . . . . . 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 737 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  ->  L  e.  NN0 )
107 elfznn0 11922 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... s )  ->  k  e.  NN0 )
108 simpll 765 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ph )
1093adantlr 726 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  A  e.  K )
110108, 81, 1093jca 1194 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  NN0 )  ->  ( ph  /\  k  e.  NN0  /\  A  e.  K ) )
111107, 110sylan2 481 . . . . . . . . . 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 2814 . . . . . . . 8  |-  ( (
ph  /\  s  e.  NN0 )  ->  A. k  e.  ( 0 ... s
) ( A  .*  ( k  .^  X
) )  e.  B
)
114113adantr 471 . . . . . . 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 12224 . . . . . . 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 18951 . . . . . 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 741 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  R  e.  Ring )
1183expcom 441 . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( k  e.  ( 0 ... s )  ->  A  e.  K
) )
122121imp 435 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  A  e.  K )
123107adantl 472 . . . . . . . . . . 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 18921 . . . . . . . . . . 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 1276 . . . . . . . . . 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 2466 . . . . . . . . . . . 12  |-  ( n  =  L  ->  (
n  =  k  <->  L  =  k ) )
127126ifbid 3915 . . . . . . . . . . 11  |-  ( n  =  L  ->  if ( n  =  k ,  A ,  .0.  )  =  if ( L  =  k ,  A ,  .0.  ) )
128127adantl 472 . . . . . . . . . 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 741 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  L  e.  NN0 )
1306, 14ring0cl 17857 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  .0.  e.  K )
13140, 130syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  .0.  e.  K )
132131ad3antrrr 741 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  /\  k  e.  ( 0 ... s
) )  ->  .0.  e.  K )
133122, 132ifcld 3936 . . . . . . . . . 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 5982 . . . . . . . . 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 4504 . . . . . . . 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 6336 . . . . . . 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 4422 . . . . . . . . . . . . . . . 16  |-  ( x  =  L  ->  (
s  <  x  <->  s  <  L ) )
138 csbeq1 3378 . . . . . . . . . . . . . . . . 17  |-  ( x  =  L  ->  [_ x  /  k ]_ A  =  [_ L  /  k ]_ A )
139138eqeq1d 2464 . . . . . . . . . . . . . . . 16  |-  ( x  =  L  ->  ( [_ x  /  k ]_ A  =  .0.  <->  [_ L  /  k ]_ A  =  .0.  ) )
140137, 139imbi12d 326 . . . . . . . . . . . . . . 15  |-  ( x  =  L  ->  (
( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) 
<->  ( s  <  L  ->  [_ L  /  k ]_ A  =  .0.  ) ) )
141140rspcva 3160 . . . . . . . . . . . . . 14  |-  ( ( L  e.  NN0  /\  A. x  e.  NN0  (
s  <  x  ->  [_ x  /  k ]_ A  =  .0.  )
)  ->  ( s  <  L  ->  [_ L  / 
k ]_ A  =  .0.  ) )
142 nfv 1772 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )
143 nfcsb1v 3391 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ k [_ L  /  k ]_ A
144143nfeq1 2616 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k
[_ L  /  k ]_ A  =  .0.
145142, 144nfan 2022 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ k ( ( ph  /\  ( s  e.  NN0  /\  s  <  L ) )  /\  [_ L  /  k ]_ A  =  .0.  )
146 elfz2nn0 11920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ( 0 ... s )  <->  ( k  e.  NN0  /\  s  e. 
NN0  /\  k  <_  s ) )
147 nn0re 10912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( k  e.  NN0  ->  k  e.  RR )
148147ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  k  e.  RR )
149 nn0re 10912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( s  e.  NN0  ->  s  e.  RR )
150149adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
s  e.  RR )
151150adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  s  e.  RR )
152 nn0re 10912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( L  e.  NN0  ->  L  e.  RR )
153152adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  L  e.  RR )
154 lelttr 9755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( k  e.  RR  /\  s  e.  RR  /\  L  e.  RR )  ->  (
( k  <_  s  /\  s  <  L )  ->  k  <  L
) )
155148, 151, 153, 154syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  ( ( k  <_  s  /\  s  <  L )  ->  k  <  L ) )
156 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  k  <  L )
157156olcd 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  ( L  <  k  \/  k  <  L ) )
158 df-ne 2635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( L  =/=  k  <->  -.  L  =  k )
159147adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
k  e.  RR )
160 lttri2 9747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( L  e.  RR  /\  k  e.  RR )  ->  ( L  =/=  k  <->  ( L  <  k  \/  k  <  L ) ) )
161152, 159, 160syl2anr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( k  e.  NN0  /\  s  e.  NN0 )  /\  L  e.  NN0 )  ->  ( L  =/=  k  <->  ( L  < 
k  \/  k  < 
L ) ) )
162161adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  ( L  =/=  k  <->  ( L  <  k  \/  k  < 
L ) ) )
163158, 162syl5bbr 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  ( -.  L  =  k  <->  ( L  <  k  \/  k  <  L ) ) )
164157, 163mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( k  e. 
NN0  /\  s  e.  NN0 )  /\  L  e. 
NN0 )  /\  k  <  L )  ->  -.  L  =  k )
165164ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( k  e.  NN0  /\  s  e.  NN0 )  -> 
( L  e.  NN0  ->  ( k  <_  s  ->  ( s  <  L  ->  -.  L  =  k ) ) ) )
168167expimpd 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( k  e.  NN0  /\  k  <_  s )  -> 
( ( s  e. 
NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) )
1711703adant2 1033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( k  e.  NN0  /\  s  e.  NN0  /\  k  <_  s )  ->  (
( s  e.  NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) )
172146, 171sylbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ( 0 ... s )  ->  (
( s  e.  NN0  /\  L  e.  NN0 )  ->  ( s  <  L  ->  -.  L  =  k ) ) )
173172expd 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  NN0  /\  s  <  L )  -> 
( ph  ->  ( k  e.  ( 0 ... s )  ->  -.  L  =  k )
) )
178177impcom 436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  -> 
( k  e.  ( 0 ... s )  ->  -.  L  =  k ) )
179178adantr 471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( k  e.  ( 0 ... s
)  ->  -.  L  =  k ) )
180179imp 435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( s  e.  NN0  /\  s  <  L ) )  /\  [_ L  /  k ]_ A  =  .0.  )  /\  k  e.  ( 0 ... s
) )  ->  -.  L  =  k )
181180iffalsed 3904 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( s  e.  NN0  /\  s  <  L ) )  /\  [_ L  /  k ]_ A  =  .0.  )  /\  k  e.  ( 0 ... s
) )  ->  if ( L  =  k ,  A ,  .0.  )  =  .0.  )
182145, 181mpteq2da 4504 . . . . . . . . . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . . . . . . . . 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 17844 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
18540, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  R  e.  Mnd )
186185adantr 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  ->  R  e.  Mnd )
187 ovex 6348 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 ... s )  e. 
_V
18814gsumz 16676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  Mnd  /\  ( 0 ... s
)  e.  _V )  ->  ( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  .0.  ) )  =  .0.  )
189186, 187, 188sylancl 673 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( s  e.  NN0  /\  s  < 
L ) )  -> 
( R  gsumg  ( k  e.  ( 0 ... s ) 
|->  .0.  ) )  =  .0.  )
190189adantr 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  ( R  gsumg  ( k  e.  ( 0 ... s )  |->  .0.  ) )  =  .0.  )
191 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( [_ L  /  k ]_ A  =  .0.  ->  [_ L  / 
k ]_ A  =  .0.  )
192191eqcomd 2468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( [_ L  /  k ]_ A  =  .0.  ->  .0.  =  [_ L  /  k ]_ A )
193192adantl 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
s  e.  NN0  /\  s  <  L ) )  /\  [_ L  / 
k ]_ A  =  .0.  )  ->  .0.  =  [_ L  /  k ]_ A )
194183, 190, 1933eqtrd 2500 . . . . . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . . . . . . 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 624 . . . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . 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 438 . . . . . . . . 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 453 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( -.  s  <  L  ->  (
( ph  /\  s  e.  NN0 )  /\  -.  s  <  L ) ) )
207206adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  A. x  e.  NN0  ( s  <  x  ->  [_ x  /  k ]_ A  =  .0.  ) )  -> 
( -.  s  < 
L  ->  ( ( ph  /\  s  e.  NN0 )  /\  -.  s  < 
L ) ) )
208185ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  ->  R  e.  Mnd )
209187a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  -> 
( 0 ... s
)  e.  _V )
210105nn0red 10960 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  RR )
211 lenlt 9743 . . . . . . . . . . . . 13  |-  ( ( L  e.  RR  /\  s  e.  RR )  ->  ( L  <_  s  <->  -.  s  <  L ) )
212210, 149, 211syl2an 484 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( L  <_  s  <->  -.  s  <  L ) )
213105ad2antrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  L  e.  NN0 )
214 simplr 767 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  s  e.  NN0 )
215 simpr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  L  <_  s )
216 elfz2nn0 11920 . . . . . . . . . . . . . 14  |-  ( L  e.  ( 0 ... s )  <->  ( L  e.  NN0  /\  s  e. 
NN0  /\  L  <_  s ) )
217213, 214, 215, 216syl3anbrc 1198 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  L  <_  s )  ->  L  e.  ( 0 ... s
) )
218217ex 440 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( L  <_  s  ->  L  e.  ( 0 ... s
) ) )
219212, 218sylbird 243 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  NN0 )  ->  ( -.  s  <  L  ->  L  e.  ( 0 ... s
) ) )
220219imp 435 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  ->  L  e.  ( 0 ... s ) )
221 eqcom 2469 . . . . . . . . . . . 12  |-  ( L  =  k  <->  k  =  L )
222 ifbi 3914 . . . . . . . . . . . 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 4502 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... s )  |->  if ( L  =  k ,  A ,  .0.  )
)  =  ( k  e.  ( 0 ... s )  |->  if ( k  =  L ,  A ,  .0.  )
)
2253, 6syl6eleq 2550 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN0 )  ->  A  e.  ( Base `  R )
)
226225ex 440 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( k  e.  NN0  ->  A  e.  ( Base `  R ) ) )
227226adantr 471 . . . . . . . . . . . . . 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 436 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  k  e.  ( 0 ... s
) )  ->  A  e.  ( Base `  R
) )
230229ralrimiva 2814 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  NN0 )  ->  A. k  e.  ( 0 ... s
) A  e.  (
Base `  R )
)
231230adantr 471 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  NN0 )  /\  -.  s  <  L )  ->  A. k  e.  (
0 ... s ) A  e.  ( Base `  R
) )
23214, 208, 209, 220, 224, 231gsummpt1n0 17652 . . . . . . . . 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 169 . . . . . . 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 2496 . . . . . 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 2500 . . . . 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 440 . . . 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 2891 . 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 189    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057   [_csb 3375   ifcif 3893   class class class wbr 4418    |-> cmpt 4477   -->wf 5601   ` cfv 5605  (class class class)co 6320    ^m cmap 7503   finSupp cfsupp 7914   RRcr 9569   0cc0 9570    < clt 9706    <_ cle 9707   NN0cn0 10903   ...cfz 11819   Basecbs 15176  Scalarcsca 15248   .scvsca 15249   0gc0g 15393    gsumg cgsu 15394   Mndcmnd 16590  .gcmg 16727  CMndccmn 17485  mulGrpcmgp 17778   Ringcrg 17835   LModclmod 18146  var1cv1 18824  Poly1cpl1 18825  coe1cco1 18826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-of 6563  df-ofr 6564  df-om 6725  df-1st 6825  df-2nd 6826  df-supp 6947  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-2o 7214  df-oadd 7217  df-er 7394  df-map 7505  df-pm 7506  df-ixp 7554  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fsupp 7915  df-oi 8056  df-card 8404  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-uz 11194  df-fz 11820  df-fzo 11953  df-seq 12252  df-hash 12554  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-sca 15261  df-vsca 15262  df-tset 15264  df-ple 15265  df-0g 15395  df-gsum 15396  df-mre 15547  df-mrc 15548  df-acs 15550  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-mhm 16637  df-submnd 16638  df-grp 16728  df-minusg 16729  df-sbg 16730  df-mulg 16731  df-subg 16869  df-ghm 16936  df-cntz 17026  df-cmn 17487  df-abl 17488  df-mgp 17779  df-ur 17791  df-ring 17837  df-subrg 18061  df-lmod 18148  df-lss 18211  df-psr 18635  df-mvr 18636  df-mpl 18637  df-opsr 18639  df-psr1 18828  df-vr1 18829  df-ply1 18830  df-coe1 18831
This theorem is referenced by:  gsumply1eq  18954  pm2mpf1lem  19873  pm2mpcoe1  19879  pm2mpmhmlem2  19898  cayleyhamilton1  19971  ply1mulgsum  40551
  Copyright terms: Public domain W3C validator