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

Theorem ply1scltm 16678
 Description: A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypotheses
Ref Expression
ply1scltm.k
ply1scltm.p Poly1
ply1scltm.x var1
ply1scltm.m
ply1scltm.n mulGrp
ply1scltm.e .g
ply1scltm.a algSc
Assertion
Ref Expression
ply1scltm

Proof of Theorem ply1scltm
StepHypRef Expression
1 ply1scltm.a . . . 4 algSc
2 ply1scltm.p . . . . 5 Poly1
32ply1sca2 16653 . . . 4 Scalar
4 df-base 13479 . . . . 5 Slot
5 ply1scltm.k . . . . 5
64, 5strfvi 13512 . . . 4
7 ply1scltm.m . . . 4
8 eqid 2438 . . . 4
91, 3, 6, 7, 8asclval 16399 . . 3
11 ply1scltm.x . . . . . 6 var1
12 eqid 2438 . . . . . 6
1311, 2, 12vr1cl 16616 . . . . 5
14 ply1scltm.n . . . . . . 7 mulGrp
1514, 12mgpbas 15659 . . . . . 6
1614, 8rngidval 15671 . . . . . 6
17 ply1scltm.e . . . . . 6 .g
1815, 16, 17mulg0 14900 . . . . 5
1913, 18syl 16 . . . 4