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 ) )