Metamath Proof Explorer

Theorem gsummoncoe1fzo

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses gsummoncoe1fzo.p 
|- P = ( Poly1 ` R )
gsummoncoe1fzo.b 
|- B = ( Base ` P )
gsummoncoe1fzo.x 
|- X = ( var1 ` R )
gsummoncoe1fzo.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
gsummoncoe1fzo.r 
|- ( ph -> R e. Ring )
gsummoncoe1fzo.k 
|- K = ( Base ` R )
gsummoncoe1fzo.m 
|- .* = ( .s ` P )
gsummoncoe1fzo.1 
|- .0. = ( 0g ` R )
gsummoncoe1fzo.a 
|- ( ph -> A. k e. ( 0 ..^ N ) A e. K )
gsummoncoe1fzo.l 
|- ( ph -> L e. ( 0 ..^ N ) )
gsummoncoe1fzo.n 
|- ( ph -> N e. NN0 )
gsummoncoe1fzo.2 
|- ( k = L -> A = C )
Assertion gsummoncoe1fzo 
|- ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = C )

Proof

Step Hyp Ref Expression
1 gsummoncoe1fzo.p 
 |-  P = ( Poly1 ` R )
2 gsummoncoe1fzo.b 
 |-  B = ( Base ` P )
3 gsummoncoe1fzo.x 
 |-  X = ( var1 ` R )
4 gsummoncoe1fzo.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
5 gsummoncoe1fzo.r 
 |-  ( ph -> R e. Ring )
6 gsummoncoe1fzo.k 
 |-  K = ( Base ` R )
7 gsummoncoe1fzo.m 
 |-  .* = ( .s ` P )
8 gsummoncoe1fzo.1 
 |-  .0. = ( 0g ` R )
9 gsummoncoe1fzo.a 
 |-  ( ph -> A. k e. ( 0 ..^ N ) A e. K )
10 gsummoncoe1fzo.l 
 |-  ( ph -> L e. ( 0 ..^ N ) )
11 gsummoncoe1fzo.n 
 |-  ( ph -> N e. NN0 )
12 gsummoncoe1fzo.2 
 |-  ( k = L -> A = C )
13 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
14 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 5 14 syl 
 |-  ( ph -> P e. Ring )
16 15 ringcmnd 
 |-  ( ph -> P e. CMnd )
17 nn0ex 
 |-  NN0 e. _V
18 17 a1i 
 |-  ( ph -> NN0 e. _V )
19 simpr 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. ( NN0 \ ( 0 ..^ N ) ) )
20 19 eldifbd 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> -. k e. ( 0 ..^ N ) )
21 20 iffalsed 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> if ( k e. ( 0 ..^ N ) , A , .0. ) = .0. )
22 21 oveq1d 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) = ( .0. .* ( k .^ X ) ) )
23 5 adantr 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> R e. Ring )
24 19 eldifad 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. NN0 )
25 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
26 25 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` P ) )
27 25 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
28 15 27 syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
29 28 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
30 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
31 3 1 2 vr1cl 
 |-  ( R e. Ring -> X e. B )
32 5 31 syl 
 |-  ( ph -> X e. B )
33 32 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> X e. B )
34 26 4 29 30 33 mulgnn0cld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k .^ X ) e. B )
35 24 34 syldan 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ( k .^ X ) e. B )
36 1 2 7 8 ply10s0 
 |-  ( ( R e. Ring /\ ( k .^ X ) e. B ) -> ( .0. .* ( k .^ X ) ) = ( 0g ` P ) )
37 23 35 36 syl2anc 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ( .0. .* ( k .^ X ) ) = ( 0g ` P ) )
38 22 37 eqtrd 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) = ( 0g ` P ) )
39 fzofi 
 |-  ( 0 ..^ N ) e. Fin
40 39 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
41 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
42 5 41 syl 
 |-  ( ph -> P e. LMod )
43 42 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> P e. LMod )
44 9 r19.21bi 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A e. K )
45 44 adantlr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k e. ( 0 ..^ N ) ) -> A e. K )
46 6 8 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
47 5 46 syl 
 |-  ( ph -> .0. e. K )
48 47 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. ( 0 ..^ N ) ) -> .0. e. K )
49 45 48 ifclda 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k e. ( 0 ..^ N ) , A , .0. ) e. K )
50 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
51 5 50 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
52 51 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
53 6 52 eqtrid 
 |-  ( ph -> K = ( Base ` ( Scalar ` P ) ) )
54 53 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> K = ( Base ` ( Scalar ` P ) ) )
55 49 54 eleqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k e. ( 0 ..^ N ) , A , .0. ) e. ( Base ` ( Scalar ` P ) ) )
56 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
57 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
58 2 56 7 57 lmodvscl 
 |-  ( ( P e. LMod /\ if ( k e. ( 0 ..^ N ) , A , .0. ) e. ( Base ` ( Scalar ` P ) ) /\ ( k .^ X ) e. B ) -> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) e. B )
59 43 55 34 58 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) e. B )
60 fzo0ssnn0 
 |-  ( 0 ..^ N ) C_ NN0
61 60 a1i 
 |-  ( ph -> ( 0 ..^ N ) C_ NN0 )
62 2 13 16 18 38 40 59 61 gsummptres2 
 |-  ( ph -> ( P gsum ( k e. NN0 |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) = ( P gsum ( k e. ( 0 ..^ N ) |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) )
63 simpr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ..^ N ) )
64 63 iftrued 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> if ( k e. ( 0 ..^ N ) , A , .0. ) = A )
65 64 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) = ( A .* ( k .^ X ) ) )
66 65 mpteq2dva 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) = ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) )
67 66 oveq2d 
 |-  ( ph -> ( P gsum ( k e. ( 0 ..^ N ) |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) = ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) )
68 62 67 eqtrd 
 |-  ( ph -> ( P gsum ( k e. NN0 |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) = ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) )
69 68 fveq2d 
 |-  ( ph -> ( coe1 ` ( P gsum ( k e. NN0 |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) ) )
70 69 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) ) ` L ) = ( ( coe1 ` ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) )
71 49 ralrimiva 
 |-  ( ph -> A. k e. NN0 if ( k e. ( 0 ..^ N ) , A , .0. ) e. K )
72 eqid 
 |-  ( k e. NN0 |-> if ( k e. ( 0 ..^ N ) , A , .0. ) ) = ( k e. NN0 |-> if ( k e. ( 0 ..^ N ) , A , .0. ) )
73 72 18 40 44 47 mptiffisupp 
 |-  ( ph -> ( k e. NN0 |-> if ( k e. ( 0 ..^ N ) , A , .0. ) ) finSupp .0. )
74 60 10 sselid 
 |-  ( ph -> L e. NN0 )
75 1 2 3 4 5 6 7 8 71 73 74 gsummoncoe1 
 |-  ( ph -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( if ( k e. ( 0 ..^ N ) , A , .0. ) .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ if ( k e. ( 0 ..^ N ) , A , .0. ) )
76 70 75 eqtr3d 
 |-  ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = [_ L / k ]_ if ( k e. ( 0 ..^ N ) , A , .0. ) )
77 eleq1 
 |-  ( k = L -> ( k e. ( 0 ..^ N ) <-> L e. ( 0 ..^ N ) ) )
78 77 12 ifbieq1d 
 |-  ( k = L -> if ( k e. ( 0 ..^ N ) , A , .0. ) = if ( L e. ( 0 ..^ N ) , C , .0. ) )
79 78 adantl 
 |-  ( ( ph /\ k = L ) -> if ( k e. ( 0 ..^ N ) , A , .0. ) = if ( L e. ( 0 ..^ N ) , C , .0. ) )
80 10 79 csbied 
 |-  ( ph -> [_ L / k ]_ if ( k e. ( 0 ..^ N ) , A , .0. ) = if ( L e. ( 0 ..^ N ) , C , .0. ) )
81 10 iftrued 
 |-  ( ph -> if ( L e. ( 0 ..^ N ) , C , .0. ) = C )
82 76 80 81 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ..^ N ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = C )