Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ply1coefsupp Structured version   Unicode version

Theorem ply1coefsupp 18463
 Description: The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 18464. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.)
Hypotheses
Ref Expression
ply1coefsupp.p Poly1
ply1coefsupp.x var1
ply1coefsupp.b
ply1coefsupp.n
ply1coefsupp.m mulGrp
ply1coefsupp.e .g
ply1coefsupp.a coe1
Assertion
Ref Expression
ply1coefsupp finSupp
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ply1coefsupp
StepHypRef Expression
1 ply1coefsupp.b . 2
2 eqid 2457 . 2 Scalar Scalar
3 ply1coefsupp.n . 2
4 ply1coefsupp.p . . . 4 Poly1
54ply1lmod 18420 . . 3
7 nn0ex 10822 . . 3
87a1i 11 . 2
94ply1ring 18416 . . . . 5
10 ply1coefsupp.m . . . . . 6 mulGrp
1110ringmgp 17331 . . . . 5
129, 11syl 16 . . . 4
14 simpr 461 . . 3
15 ply1coefsupp.x . . . . 5 var1
1615, 4, 1vr1cl 18385 . . . 4
1810, 1mgpbas 17274 . . . 4
19 ply1coefsupp.e . . . 4 .g
2018, 19mulgnn0cl 16285 . . 3
2113, 14, 17, 20syl3anc 1228 . 2
22 ply1coefsupp.a . . . 4 coe1
23 eqid 2457 . . . 4
2422, 1, 4, 23coe1f 18377 . . 3