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 5 3 mgpbas
 |-  B = ( Base ` M )
14 1 ply1ring
 |-  ( R e. Ring -> P e. Ring )
15 5 ringmgp
 |-  ( P e. Ring -> M e. Mnd )
16 14 15 syl
 |-  ( R e. Ring -> M e. Mnd )
17 16 ad2antrr
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> M e. Mnd )
18 simpr
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> k e. NN0 )
19 2 1 3 vr1cl
 |-  ( R e. Ring -> X e. B )
20 19 ad2antrr
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> X e. B )
21 13 6 17 18 20 mulgnn0cld
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. B )
22 eqid
 |-  ( Base ` R ) = ( Base ` R )
23 7 3 1 22 coe1f
 |-  ( K e. B -> A : NN0 --> ( Base ` R ) )
24 23 adantl
 |-  ( ( R e. Ring /\ K e. B ) -> A : NN0 --> ( Base ` R ) )
25 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
26 7 3 1 25 coe1sfi
 |-  ( K e. B -> A finSupp ( 0g ` R ) )
27 26 adantl
 |-  ( ( R e. Ring /\ K e. B ) -> A finSupp ( 0g ` R ) )
28 1 ply1sca
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
29 28 eqcomd
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
30 29 adantr
 |-  ( ( R e. Ring /\ K e. B ) -> ( Scalar ` P ) = R )
31 30 fveq2d
 |-  ( ( R e. Ring /\ K e. B ) -> ( 0g ` ( Scalar ` P ) ) = ( 0g ` R ) )
32 27 31 breqtrrd
 |-  ( ( R e. Ring /\ K e. B ) -> A finSupp ( 0g ` ( Scalar ` P ) ) )
33 3 8 4 10 12 21 24 32 mptscmfsuppd
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )