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

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