Metamath Proof Explorer

Theorem coe1tmmul

Description: Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses coe1tm.z ⊢ 0 = ( 0g ‘ 𝑅 )
coe1tm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
coe1tm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1tm.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
coe1tm.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
coe1tm.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
coe1tm.e ⊢ ↑ = ( .g ‘ 𝑁 )
coe1tmmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
coe1tmmul.t ⊢ ∙ = ( .r ‘ 𝑃 )
coe1tmmul.u ⊢ × = ( .r ‘ 𝑅 )
coe1tmmul.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
coe1tmmul.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
coe1tmmul.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
coe1tmmul.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
Assertion coe1tmmul ( 𝜑 → ( coe1 ‘ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∙ 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 coe1tm.z ⊢ 0 = ( 0g ‘ 𝑅 )
2 coe1tm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 coe1tm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 coe1tm.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 coe1tm.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
6 coe1tm.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7 coe1tm.e ⊢ ↑ = ( .g ‘ 𝑁 )
8 coe1tmmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
9 coe1tmmul.t ⊢ ∙ = ( .r ‘ 𝑃 )
10 coe1tmmul.u ⊢ × = ( .r ‘ 𝑅 )
11 coe1tmmul.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
12 coe1tmmul.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
13 coe1tmmul.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
14 coe1tmmul.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
15 2 3 4 5 6 7 8 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )
16 12 13 14 15 syl3anc ⊢ ( 𝜑 → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )
17 3 9 10 8 coe1mul ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∙ 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) )
18 12 16 11 17 syl3anc ⊢ ( 𝜑 → ( coe1 ‘ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∙ 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) )
19 eqeq2 ⊢ ( ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) = if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) → ( ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) ↔ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )
20 eqeq2 ⊢ ( 0 = if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) → ( ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = 0 ↔ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )
21 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝑅 ∈ Ring )
22 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
23 21 22 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝑅 ∈ Mnd )
24 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 0 ... 𝑥 ) ∈ V )
25 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ∈ ℕ0 )
26 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ≤ 𝑥 )
27 fznn0 ⊢ ( 𝑥 ∈ ℕ0 → ( 𝐷 ∈ ( 0 ... 𝑥 ) ↔ ( 𝐷 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) )
28 27 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝐷 ∈ ( 0 ... 𝑥 ) ↔ ( 𝐷 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) )
29 25 26 28 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ∈ ( 0 ... 𝑥 ) )
30 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑅 ∈ Ring )
31 eqid ⊢ ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) )
32 31 8 3 2 coe1f ⊢ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 )
33 16 32 syl ⊢ ( 𝜑 → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 )
35 elfznn0 ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℕ0 )
36 ffvelcdm ⊢ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 ∧ 𝑦 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) ∈ 𝐾 )
37 34 35 36 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) ∈ 𝐾 )
38 eqid ⊢ ( coe1 ‘ 𝐴 ) = ( coe1 ‘ 𝐴 )
39 38 8 3 2 coe1f ⊢ ( 𝐴 ∈ 𝐵 → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
40 11 39 syl ⊢ ( 𝜑 → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
42 fznn0sub ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → ( 𝑥 − 𝑦 ) ∈ ℕ0 )
43 ffvelcdm ⊢ ( ( ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 ∧ ( 𝑥 − 𝑦 ) ∈ ℕ0 ) → ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ∈ 𝐾 )
44 41 42 43 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ∈ 𝐾 )
45 2 10 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) ∈ 𝐾 ∧ ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ∈ 𝐾 ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ∈ 𝐾 )
46 30 37 44 45 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ∈ 𝐾 )
47 46 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) : ( 0 ... 𝑥 ) ⟶ 𝐾 )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) : ( 0 ... 𝑥 ) ⟶ 𝐾 )
49 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝑅 ∈ Ring )
50 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝐶 ∈ 𝐾 )
51 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝐷 ∈ ℕ0 )
52 eldifi ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝑦 ∈ ( 0 ... 𝑥 ) )
53 52 35 syl ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝑦 ∈ ℕ0 )
54 53 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝑦 ∈ ℕ0 )
55 eldifsni ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝑦 ≠ 𝐷 )
56 55 necomd ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝐷 ≠ 𝑦 )
57 56 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝐷 ≠ 𝑦 )
58 1 2 3 4 5 6 7 49 50 51 54 57 coe1tmfv2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) = 0 )
59 58 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) )
60 2 10 1 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ∈ 𝐾 ) → ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
61 30 44 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
62 52 61 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
63 62 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
64 59 63 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
65 64 24 suppss2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) supp 0 ) ⊆ { 𝐷 } )
66 2 1 23 24 29 48 65 gsumpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ 𝐷 ) )
67 fveq2 ⊢ ( 𝑦 = 𝐷 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) = ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) )
68 oveq2 ⊢ ( 𝑦 = 𝐷 → ( 𝑥 − 𝑦 ) = ( 𝑥 − 𝐷 ) )
69 68 fveq2d ⊢ ( 𝑦 = 𝐷 → ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) = ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) )
70 67 69 oveq12d ⊢ ( 𝑦 = 𝐷 → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) )
71 eqid ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) )
72 ovex ⊢ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) ∈ V
73 70 71 72 fvmpt ⊢ ( 𝐷 ∈ ( 0 ... 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ 𝐷 ) = ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) )
74 29 73 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ 𝐷 ) = ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) )
75 1 2 3 4 5 6 7 coe1tmfv1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
76 12 13 14 75 syl3anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
77 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
78 77 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) = ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) )
79 74 78 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ 𝐷 ) = ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) )
80 66 79 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) )
81 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑅 ∈ Ring )
82 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝐶 ∈ 𝐾 )
83 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝐷 ∈ ℕ0 )
84 35 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ∈ ℕ0 )
85 elfzle2 ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ≤ 𝑥 )
86 85 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ≤ 𝑥 )
87 breq1 ⊢ ( 𝐷 = 𝑦 → ( 𝐷 ≤ 𝑥 ↔ 𝑦 ≤ 𝑥 ) )
88 86 87 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝐷 = 𝑦 → 𝐷 ≤ 𝑥 ) )
89 88 necon3bd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ¬ 𝐷 ≤ 𝑥 → 𝐷 ≠ 𝑦 ) )
90 89 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ∧ ¬ 𝐷 ≤ 𝑥 ) → 𝐷 ≠ 𝑦 )
91 90 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝐷 ≠ 𝑦 )
92 1 2 3 4 5 6 7 81 82 83 84 91 coe1tmfv2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) = 0 )
93 92 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) )
94 61 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 0 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
95 93 94 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
96 95 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) )
97 96 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) )
98 12 22 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → 𝑅 ∈ Mnd )
100 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 0 ... 𝑥 ) ∈ V )
101 1 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑥 ) ∈ V ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
102 99 100 101 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
103 97 102 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = 0 )
104 19 20 80 103 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) )
105 104 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )
106 18 105 eqtrd ⊢ ( 𝜑 → ( coe1 ‘ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∙ 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )