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 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
25 4 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
26 8 24 25 3syl ⊢ ( 𝜑 → 𝑁 ∈ Mnd )
27 3 2 6 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
28 8 27 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
29 4 6 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑁 )
30 29 5 mulgnn0cl ⊢ ( ( 𝑁 ∈ Mnd ∧ 𝐷 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )
31 26 10 28 30 syl3anc ⊢ ( 𝜑 → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )
32 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
33 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
34 6 32 12 33 lmodvs1 ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( 𝐷 ↑ 𝑋 ) )
35 23 31 34 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( 𝐷 ↑ 𝑋 ) )
36 21 35 eqtrd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( 𝐷 ↑ 𝑋 ) )
37 36 fvoveq1d ⊢ ( 𝜑 → ( coe1 ‘ ( ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) · 𝐴 ) ) = ( coe1 ‘ ( ( 𝐷 ↑ 𝑋 ) · 𝐴 ) ) )
38 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝑅 ∈ Ring )
39 eqid ⊢ ( coe1 ‘ 𝐴 ) = ( coe1 ‘ 𝐴 )
40 39 6 2 11 coe1f ⊢ ( 𝐴 ∈ 𝐵 → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
41 9 40 syl ⊢ ( 𝜑 → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
43 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ∈ ℕ0 )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝑥 ∈ ℕ0 )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ≤ 𝑥 )
46 nn0sub2 ⊢ ( ( 𝐷 ∈ ℕ0 ∧ 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) → ( 𝑥 − 𝐷 ) ∈ ℕ0 )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝑥 − 𝐷 ) ∈ ℕ0 )
48 42 47 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ∈ ( Base ‘ 𝑅 ) )
49 11 13 14 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) = ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) )
50 38 48 49 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) = ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) )
51 50 ifeq1da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → if ( 𝐷 ≤ 𝑥 , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) = if ( 𝐷 ≤ 𝑥 , ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) )
52 51 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) ) )
53 17 37 52 3eqtr3d ⊢ ( 𝜑 → ( coe1 ‘ ( ( 𝐷 ↑ 𝑋 ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) ) )