Metamath Proof Explorer


Theorem ply1coefsupp

Description: The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe . (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 8-Aug-2019)

Ref Expression
Hypotheses ply1coefsupp.p
|- P = ( Poly1 ` R )
ply1coefsupp.x
|- X = ( var1 ` R )
ply1coefsupp.b
|- B = ( Base ` P )
ply1coefsupp.n
|- .x. = ( .s ` P )
ply1coefsupp.m
|- M = ( mulGrp ` P )
ply1coefsupp.e
|- .^ = ( .g ` M )
ply1coefsupp.a
|- A = ( coe1 ` K )
Assertion ply1coefsupp
|- ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )

Proof

Step Hyp Ref Expression
1 ply1coefsupp.p
 |-  P = ( Poly1 ` R )
2 ply1coefsupp.x
 |-  X = ( var1 ` R )
3 ply1coefsupp.b
 |-  B = ( Base ` P )
4 ply1coefsupp.n
 |-  .x. = ( .s ` P )
5 ply1coefsupp.m
 |-  M = ( mulGrp ` P )
6 ply1coefsupp.e
 |-  .^ = ( .g ` M )
7 ply1coefsupp.a
 |-  A = ( coe1 ` K )
8 eqid
 |-  ( Scalar ` P ) = ( Scalar ` P )
9 1 ply1lmod
 |-  ( R e. Ring -> P e. LMod )
10 9 adantr
 |-  ( ( R e. Ring /\ K e. B ) -> P e. LMod )
11 nn0ex
 |-  NN0 e. _V
12 11 a1i
 |-  ( ( R e. Ring /\ K e. B ) -> NN0 e. _V )
13 1 ply1ring
 |-  ( R e. Ring -> P e. Ring )
14 5 ringmgp
 |-  ( P e. Ring -> M e. Mnd )
15 13 14 syl
 |-  ( R e. Ring -> M e. Mnd )
16 15 ad2antrr
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> M e. Mnd )
17 simpr
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> k e. NN0 )
18 2 1 3 vr1cl
 |-  ( R e. Ring -> X e. B )
19 18 ad2antrr
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> X e. B )
20 5 3 mgpbas
 |-  B = ( Base ` M )
21 20 6 mulgnn0cl
 |-  ( ( M e. Mnd /\ k e. NN0 /\ X e. B ) -> ( k .^ X ) e. B )
22 16 17 19 21 syl3anc
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. B )
23 eqid
 |-  ( Base ` R ) = ( Base ` R )
24 7 3 1 23 coe1f
 |-  ( K e. B -> A : NN0 --> ( Base ` R ) )
25 24 adantl
 |-  ( ( R e. Ring /\ K e. B ) -> A : NN0 --> ( Base ` R ) )
26 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
27 7 3 1 26 coe1sfi
 |-  ( K e. B -> A finSupp ( 0g ` R ) )
28 27 adantl
 |-  ( ( R e. Ring /\ K e. B ) -> A finSupp ( 0g ` R ) )
29 1 ply1sca
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
30 29 eqcomd
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
31 30 adantr
 |-  ( ( R e. Ring /\ K e. B ) -> ( Scalar ` P ) = R )
32 31 fveq2d
 |-  ( ( R e. Ring /\ K e. B ) -> ( 0g ` ( Scalar ` P ) ) = ( 0g ` R ) )
33 28 32 breqtrrd
 |-  ( ( R e. Ring /\ K e. B ) -> A finSupp ( 0g ` ( Scalar ` P ) ) )
34 3 8 4 10 12 22 25 33 mptscmfsuppd
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )