Metamath Proof Explorer


Theorem gsumsmonply1

Description: A finite group sum of scaled monomials is a univariate polynomial. (Contributed by AV, 8-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. )
Assertion gsumsmonply1
|- ( ph -> ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) e. B )

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 eqid
 |-  ( 0g ` P ) = ( 0g ` P )
12 1 ply1ring
 |-  ( R e. Ring -> P e. Ring )
13 ringcmn
 |-  ( P e. Ring -> P e. CMnd )
14 5 12 13 3syl
 |-  ( ph -> P e. CMnd )
15 nn0ex
 |-  NN0 e. _V
16 15 a1i
 |-  ( ph -> NN0 e. _V )
17 9 r19.21bi
 |-  ( ( ph /\ k e. NN0 ) -> A e. K )
18 5 3ad2ant1
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> R e. Ring )
19 simp3
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> A e. K )
20 simp2
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> k e. NN0 )
21 eqid
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
22 6 1 3 7 21 4 2 ply1tmcl
 |-  ( ( R e. Ring /\ A e. K /\ k e. NN0 ) -> ( A .* ( k .^ X ) ) e. B )
23 18 19 20 22 syl3anc
 |-  ( ( ph /\ k e. NN0 /\ A e. K ) -> ( A .* ( k .^ X ) ) e. B )
24 17 23 mpd3an3
 |-  ( ( ph /\ k e. NN0 ) -> ( A .* ( k .^ X ) ) e. B )
25 24 fmpttd
 |-  ( ph -> ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) : NN0 --> B )
26 1 ply1lmod
 |-  ( R e. Ring -> P e. LMod )
27 5 26 syl
 |-  ( ph -> P e. LMod )
28 1 ply1sca
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
29 5 28 syl
 |-  ( ph -> R = ( Scalar ` P ) )
30 1 3 21 4 2 ply1moncl
 |-  ( ( R e. Ring /\ k e. NN0 ) -> ( k .^ X ) e. B )
31 5 30 sylan
 |-  ( ( ph /\ k e. NN0 ) -> ( k .^ X ) e. B )
32 16 27 29 2 17 31 11 8 7 10 mptscmfsupp0
 |-  ( ph -> ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) finSupp ( 0g ` P ) )
33 2 11 14 16 25 32 gsumcl
 |-  ( ph -> ( P gsum ( k e. NN0 |-> ( A .* ( k .^ X ) ) ) ) e. B )