Metamath Proof Explorer

Theorem coe1pwmul

Description: Coefficient vector of a polynomial multiplied on the left by a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses coe1pwmul.z 
|- .0. = ( 0g ` R )
coe1pwmul.p 
|- P = ( Poly1 ` R )
coe1pwmul.x 
|- X = ( var1 ` R )
coe1pwmul.n 
|- N = ( mulGrp ` P )
coe1pwmul.e 
|- .^ = ( .g ` N )
coe1pwmul.b 
|- B = ( Base ` P )
coe1pwmul.t 
|- .x. = ( .r ` P )
coe1pwmul.r 
|- ( ph -> R e. Ring )
coe1pwmul.a 
|- ( ph -> A e. B )
coe1pwmul.d 
|- ( ph -> D e. NN0 )
Assertion coe1pwmul 
|- ( ph -> ( coe1 ` ( ( D .^ X ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) )

Proof

Step Hyp Ref Expression
1 coe1pwmul.z 
 |-  .0. = ( 0g ` R )
2 coe1pwmul.p 
 |-  P = ( Poly1 ` R )
3 coe1pwmul.x 
 |-  X = ( var1 ` R )
4 coe1pwmul.n 
 |-  N = ( mulGrp ` P )
5 coe1pwmul.e 
 |-  .^ = ( .g ` N )
6 coe1pwmul.b 
 |-  B = ( Base ` P )
7 coe1pwmul.t 
 |-  .x. = ( .r ` P )
8 coe1pwmul.r 
 |-  ( ph -> R e. Ring )
9 coe1pwmul.a 
 |-  ( ph -> A e. B )
10 coe1pwmul.d 
 |-  ( ph -> D e. NN0 )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  ( .s ` P ) = ( .s ` P )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
15 11 14 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
16 8 15 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
17 1 11 2 3 12 4 5 6 7 13 9 8 16 10 coe1tmmul 
 |-  ( ph -> ( coe1 ` ( ( ( 1r ` R ) ( .s ` P ) ( D .^ X ) ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( 1r ` R ) ( .r ` R ) ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )
18 2 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
19 8 18 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
20 19 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
21 20 oveq1d 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( D .^ X ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( D .^ X ) ) )
22 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
23 8 22 syl 
 |-  ( ph -> P e. LMod )
24 4 6 mgpbas 
 |-  B = ( Base ` N )
25 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
26 4 ringmgp 
 |-  ( P e. Ring -> N e. Mnd )
27 8 25 26 3syl 
 |-  ( ph -> N e. Mnd )
28 3 2 6 vr1cl 
 |-  ( R e. Ring -> X e. B )
29 8 28 syl 
 |-  ( ph -> X e. B )
30 24 5 27 10 29 mulgnn0cld 
 |-  ( ph -> ( D .^ X ) e. B )
31 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
32 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
33 6 31 12 32 lmodvs1 
 |-  ( ( P e. LMod /\ ( D .^ X ) e. B ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( D .^ X ) ) = ( D .^ X ) )
34 23 30 33 syl2anc 
 |-  ( ph -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( D .^ X ) ) = ( D .^ X ) )
35 21 34 eqtrd 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( D .^ X ) ) = ( D .^ X ) )
36 35 fvoveq1d 
 |-  ( ph -> ( coe1 ` ( ( ( 1r ` R ) ( .s ` P ) ( D .^ X ) ) .x. A ) ) = ( coe1 ` ( ( D .^ X ) .x. A ) ) )
37 8 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> R e. Ring )
38 eqid 
 |-  ( coe1 ` A ) = ( coe1 ` A )
39 38 6 2 11 coe1f 
 |-  ( A e. B -> ( coe1 ` A ) : NN0 --> ( Base ` R ) )
40 9 39 syl 
 |-  ( ph -> ( coe1 ` A ) : NN0 --> ( Base ` R ) )
41 40 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( coe1 ` A ) : NN0 --> ( Base ` R ) )
42 10 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D e. NN0 )
43 simplr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> x e. NN0 )
44 simpr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D <_ x )
45 nn0sub2 
 |-  ( ( D e. NN0 /\ x e. NN0 /\ D <_ x ) -> ( x - D ) e. NN0 )
46 42 43 44 45 syl3anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( x - D ) e. NN0 )
47 41 46 ffvelcdmd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( coe1 ` A ) ` ( x - D ) ) e. ( Base ` R ) )
48 11 13 14 ringlidm 
 |-  ( ( R e. Ring /\ ( ( coe1 ` A ) ` ( x - D ) ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( ( coe1 ` A ) ` ( x - D ) ) ) = ( ( coe1 ` A ) ` ( x - D ) ) )
49 37 47 48 syl2anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( 1r ` R ) ( .r ` R ) ( ( coe1 ` A ) ` ( x - D ) ) ) = ( ( coe1 ` A ) ` ( x - D ) ) )
50 49 ifeq1da 
 |-  ( ( ph /\ x e. NN0 ) -> if ( D <_ x , ( ( 1r ` R ) ( .r ` R ) ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) = if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) )
51 50 mpteq2dva 
 |-  ( ph -> ( x e. NN0 |-> if ( D <_ x , ( ( 1r ` R ) ( .r ` R ) ( ( coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) )
52 17 36 51 3eqtr3d 
 |-  ( ph -> ( coe1 ` ( ( D .^ X ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) )