Metamath Proof Explorer

Theorem ply1scltm

Description: A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses ply1scltm.k 
|- K = ( Base ` R )
ply1scltm.p 
|- P = ( Poly1 ` R )
ply1scltm.x 
|- X = ( var1 ` R )
ply1scltm.m 
|- .x. = ( .s ` P )
ply1scltm.n 
|- N = ( mulGrp ` P )
ply1scltm.e 
|- .^ = ( .g ` N )
ply1scltm.a 
|- A = ( algSc ` P )
Assertion ply1scltm 
|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) )

Proof

Step Hyp Ref Expression
1 ply1scltm.k 
 |-  K = ( Base ` R )
2 ply1scltm.p 
 |-  P = ( Poly1 ` R )
3 ply1scltm.x 
 |-  X = ( var1 ` R )
4 ply1scltm.m 
 |-  .x. = ( .s ` P )
5 ply1scltm.n 
 |-  N = ( mulGrp ` P )
6 ply1scltm.e 
 |-  .^ = ( .g ` N )
7 ply1scltm.a 
 |-  A = ( algSc ` P )
8 2 ply1sca2 
 |-  ( _I ` R ) = ( Scalar ` P )
9 df-base 
 |-  Base = Slot 1
10 9 1 strfvi 
 |-  K = ( Base ` ( _I ` R ) )
11 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
12 7 8 10 4 11 asclval 
 |-  ( F e. K -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
13 12 adantl 
 |-  ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
14 eqid 
 |-  ( Base ` P ) = ( Base ` P )
15 3 2 14 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
16 5 14 mgpbas 
 |-  ( Base ` P ) = ( Base ` N )
17 5 11 ringidval 
 |-  ( 1r ` P ) = ( 0g ` N )
18 16 17 6 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
19 15 18 syl 
 |-  ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) )
20 19 adantr 
 |-  ( ( R e. Ring /\ F e. K ) -> ( 0 .^ X ) = ( 1r ` P ) )
21 20 oveq2d 
 |-  ( ( R e. Ring /\ F e. K ) -> ( F .x. ( 0 .^ X ) ) = ( F .x. ( 1r ` P ) ) )
22 13 21 eqtr4d 
 |-  ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) )