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 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
25 4 ringmgp 
 |-  ( P e. Ring -> N e. Mnd )
26 8 24 25 3syl 
 |-  ( ph -> N e. Mnd )
27 3 2 6 vr1cl 
 |-  ( R e. Ring -> X e. B )
28 8 27 syl 
 |-  ( ph -> X e. B )
29 4 6 mgpbas 
 |-  B = ( Base ` N )
30 29 5 mulgnn0cl 
 |-  ( ( N e. Mnd /\ D e. NN0 /\ X e. B ) -> ( D .^ X ) e. B )
31 26 10 28 30 syl3anc 
 |-  ( ph -> ( D .^ X ) e. B )
32 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
33 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
34 6 32 12 33 lmodvs1 
 |-  ( ( P e. LMod /\ ( D .^ X ) e. B ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( D .^ X ) ) = ( D .^ X ) )
35 23 31 34 syl2anc 
 |-  ( ph -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( D .^ X ) ) = ( D .^ X ) )
36 21 35 eqtrd 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( D .^ X ) ) = ( D .^ X ) )
37 36 fvoveq1d 
 |-  ( ph -> ( coe1 ` ( ( ( 1r ` R ) ( .s ` P ) ( D .^ X ) ) .x. A ) ) = ( coe1 ` ( ( D .^ X ) .x. A ) ) )
38 8 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> R e. Ring )
39 eqid 
 |-  ( coe1 ` A ) = ( coe1 ` A )
40 39 6 2 11 coe1f 
 |-  ( A e. B -> ( coe1 ` A ) : NN0 --> ( Base ` R ) )
41 9 40 syl 
 |-  ( ph -> ( coe1 ` A ) : NN0 --> ( Base ` R ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( coe1 ` A ) : NN0 --> ( Base ` R ) )
43 10 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D e. NN0 )
44 simplr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> x e. NN0 )
45 simpr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> D <_ x )
46 nn0sub2 
 |-  ( ( D e. NN0 /\ x e. NN0 /\ D <_ x ) -> ( x - D ) e. NN0 )
47 43 44 45 46 syl3anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( x - D ) e. NN0 )
48 42 47 ffvelrnd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( coe1 ` A ) ` ( x - D ) ) e. ( Base ` R ) )
49 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 ) ) )
50 38 48 49 syl2anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ D <_ x ) -> ( ( 1r ` R ) ( .r ` R ) ( ( coe1 ` A ) ` ( x - D ) ) ) = ( ( coe1 ` A ) ` ( x - D ) ) )
51 50 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. ) )
52 51 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. ) ) )
53 17 37 52 3eqtr3d 
 |-  ( ph -> ( coe1 ` ( ( D .^ X ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) )