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

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 )