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𝑅 )
coe1pwmul.p 𝑃 = ( Poly1𝑅 )
coe1pwmul.x 𝑋 = ( var1𝑅 )
coe1pwmul.n 𝑁 = ( mulGrp ‘ 𝑃 )
coe1pwmul.e = ( .g𝑁 )
coe1pwmul.b 𝐵 = ( Base ‘ 𝑃 )
coe1pwmul.t · = ( .r𝑃 )
coe1pwmul.r ( 𝜑𝑅 ∈ Ring )
coe1pwmul.a ( 𝜑𝐴𝐵 )
coe1pwmul.d ( 𝜑𝐷 ∈ ℕ0 )
Assertion coe1pwmul ( 𝜑 → ( coe1 ‘ ( ( 𝐷 𝑋 ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 coe1pwmul.z 0 = ( 0g𝑅 )
2 coe1pwmul.p 𝑃 = ( Poly1𝑅 )
3 coe1pwmul.x 𝑋 = ( var1𝑅 )
4 coe1pwmul.n 𝑁 = ( mulGrp ‘ 𝑃 )
5 coe1pwmul.e = ( .g𝑁 )
6 coe1pwmul.b 𝐵 = ( Base ‘ 𝑃 )
7 coe1pwmul.t · = ( .r𝑃 )
8 coe1pwmul.r ( 𝜑𝑅 ∈ Ring )
9 coe1pwmul.a ( 𝜑𝐴𝐵 )
10 coe1pwmul.d ( 𝜑𝐷 ∈ ℕ0 )
11 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 eqid ( ·𝑠𝑃 ) = ( ·𝑠𝑃 )
13 eqid ( .r𝑅 ) = ( .r𝑅 )
14 eqid ( 1r𝑅 ) = ( 1r𝑅 )
15 11 14 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
16 8 15 syl ( 𝜑 → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
17 1 11 2 3 12 4 5 6 7 13 9 8 16 10 coe1tmmul ( 𝜑 → ( coe1 ‘ ( ( ( 1r𝑅 ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( 1r𝑅 ) ( .r𝑅 ) ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) , 0 ) ) )
18 2 ply1sca ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
19 8 18 syl ( 𝜑𝑅 = ( Scalar ‘ 𝑃 ) )
20 19 fveq2d ( 𝜑 → ( 1r𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
21 20 oveq1d ( 𝜑 → ( ( 1r𝑅 ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) )
22 2 ply1lmod ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
23 8 22 syl ( 𝜑𝑃 ∈ LMod )
24 4 6 mgpbas 𝐵 = ( Base ‘ 𝑁 )
25 2 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
26 4 ringmgp ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
27 8 25 26 3syl ( 𝜑𝑁 ∈ Mnd )
28 3 2 6 vr1cl ( 𝑅 ∈ Ring → 𝑋𝐵 )
29 8 28 syl ( 𝜑𝑋𝐵 )
30 24 5 27 10 29 mulgnn0cld ( 𝜑 → ( 𝐷 𝑋 ) ∈ 𝐵 )
31 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
32 eqid ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
33 6 31 12 32 lmodvs1 ( ( 𝑃 ∈ LMod ∧ ( 𝐷 𝑋 ) ∈ 𝐵 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) = ( 𝐷 𝑋 ) )
34 23 30 33 syl2anc ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) = ( 𝐷 𝑋 ) )
35 21 34 eqtrd ( 𝜑 → ( ( 1r𝑅 ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) = ( 𝐷 𝑋 ) )
36 35 fvoveq1d ( 𝜑 → ( coe1 ‘ ( ( ( 1r𝑅 ) ( ·𝑠𝑃 ) ( 𝐷 𝑋 ) ) · 𝐴 ) ) = ( coe1 ‘ ( ( 𝐷 𝑋 ) · 𝐴 ) ) )
37 8 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝑅 ∈ Ring )
38 eqid ( coe1𝐴 ) = ( coe1𝐴 )
39 38 6 2 11 coe1f ( 𝐴𝐵 → ( coe1𝐴 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
40 9 39 syl ( 𝜑 → ( coe1𝐴 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
41 40 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( coe1𝐴 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
42 10 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝐷 ∈ ℕ0 )
43 simplr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝑥 ∈ ℕ0 )
44 simpr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝐷𝑥 )
45 nn0sub2 ( ( 𝐷 ∈ ℕ0𝑥 ∈ ℕ0𝐷𝑥 ) → ( 𝑥𝐷 ) ∈ ℕ0 )
46 42 43 44 45 syl3anc ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 𝑥𝐷 ) ∈ ℕ0 )
47 41 46 ffvelcdmd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ∈ ( Base ‘ 𝑅 ) )
48 11 13 14 ringlidm ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r𝑅 ) ( .r𝑅 ) ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) = ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) )
49 37 47 48 syl2anc ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( 1r𝑅 ) ( .r𝑅 ) ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) = ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) )
50 49 ifeq1da ( ( 𝜑𝑥 ∈ ℕ0 ) → if ( 𝐷𝑥 , ( ( 1r𝑅 ) ( .r𝑅 ) ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) , 0 ) = if ( 𝐷𝑥 , ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) , 0 ) )
51 50 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( 1r𝑅 ) ( .r𝑅 ) ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) , 0 ) ) )
52 17 36 51 3eqtr3d ( 𝜑 → ( coe1 ‘ ( ( 𝐷 𝑋 ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) , 0 ) ) )