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

Theorem smon1ply1 30983
 Description: A scaled univariate monomial is a univariate polynomial. (Contributed by AV, 8-Oct-2019.)
Hypotheses
Ref Expression
gsummonply1.p Poly1
gsummonply1.b
gsummonply1.x var1
gsummonply1.e .gmulGrp
gsummonply1.r
gsummonply1.k
gsummonply1.m
Assertion
Ref Expression
smon1ply1

Proof of Theorem smon1ply1
StepHypRef Expression
1 gsummonply1.r . . . 4
2 gsummonply1.p . . . . 5 Poly1
32ply1lmod 17814 . . . 4
41, 3syl 16 . . 3
6 gsummonply1.k . . . . . . 7
72ply1sca 17815 . . . . . . . . 9 Scalar
81, 7syl 16 . . . . . . . 8 Scalar
98fveq2d 5793 . . . . . . 7 Scalar
106, 9syl5eq 2504 . . . . . 6 Scalar
1110eleq2d 2521 . . . . 5 Scalar
1211biimpd 207 . . . 4 Scalar
1312a1d 25 . . 3 Scalar
14133imp 1182 . 2 Scalar
15 gsummonply1.b . . . 4
16 gsummonply1.x . . . 4 var1
17 gsummonply1.e . . . 4 .gmulGrp
182, 15, 16, 17, 1mon1ply1 30982 . . 3