Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ply1coefsupp Structured version   Unicode version

Theorem ply1coefsupp 30735
 Description: The decomposition of a univariate polynomial is finitely supported. Part of proof for ply1coe 17720 which could be shortened (TODO). (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 2441 . 2 Scalar Scalar
3 ply1coefsupp.n . 2
4 ply1coefsupp.p . . . 4 Poly1
54ply1lmod 17682 . . 3
7 nn0ex 10581 . . 3
87a1i 11 . 2
94ply1rng 17678 . . . . 5
10 ply1coefsupp.m . . . . . 6 mulGrp
1110rngmgp 16641 . . . . 5
129, 11syl 16 . . . 4
14 simpr 458 . . 3
15 ply1coefsupp.x . . . . 5 var1
1615, 4, 1vr1cl 17647 . . . 4
1810, 1mgpbas 16587 . . . 4
19 ply1coefsupp.e . . . 4 .g
2018, 19mulgnn0cl 15636 . . 3
2113, 14, 17, 20syl3anc 1213 . 2
22 ply1coefsupp.a . . . 4 coe1
23 eqid 2441 . . . 4
2422, 1, 4, 23coe1f 17643 . . 3