Metamath Proof Explorer

Theorem coe1tmmul2

Description: Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-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 coe1tmmul2 ( 𝜑 → ( 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 11 16 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 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑅 ∈ Ring )
22 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
23 21 22 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑅 ∈ Mnd )
24 ovex ⊢ ( 0 ... 𝑥 ) ∈ V
25 24 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 0 ... 𝑥 ) ∈ V )
26 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐷 ≤ 𝑥 )
27 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐷 ∈ ℕ0 )
28 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ ℕ0 )
29 nn0sub ⊢ ( ( 𝐷 ∈ ℕ0 ∧ 𝑥 ∈ ℕ0 ) → ( 𝐷 ≤ 𝑥 ↔ ( 𝑥 − 𝐷 ) ∈ ℕ0 ) )
30 27 28 29 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝐷 ≤ 𝑥 ↔ ( 𝑥 − 𝐷 ) ∈ ℕ0 ) )
31 26 30 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 − 𝐷 ) ∈ ℕ0 )
32 27 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐷 )
33 nn0re ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ )
34 33 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
35 14 nn0red ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐷 ∈ ℝ )
37 34 36 subge02d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 0 ≤ 𝐷 ↔ ( 𝑥 − 𝐷 ) ≤ 𝑥 ) )
38 32 37 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 − 𝐷 ) ≤ 𝑥 )
39 fznn0 ⊢ ( 𝑥 ∈ ℕ0 → ( ( 𝑥 − 𝐷 ) ∈ ( 0 ... 𝑥 ) ↔ ( ( 𝑥 − 𝐷 ) ∈ ℕ0 ∧ ( 𝑥 − 𝐷 ) ≤ 𝑥 ) ) )
40 39 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( 𝑥 − 𝐷 ) ∈ ( 0 ... 𝑥 ) ↔ ( ( 𝑥 − 𝐷 ) ∈ ℕ0 ∧ ( 𝑥 − 𝐷 ) ≤ 𝑥 ) ) )
41 31 38 40 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 − 𝐷 ) ∈ ( 0 ... 𝑥 ) )
42 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑅 ∈ Ring )
43 eqid ⊢ ( coe1 ‘ 𝐴 ) = ( coe1 ‘ 𝐴 )
44 43 8 3 2 coe1f ⊢ ( 𝐴 ∈ 𝐵 → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
45 11 44 syl ⊢ ( 𝜑 → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
47 elfznn0 ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℕ0 )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ∈ ℕ0 )
49 46 48 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) ∈ 𝐾 )
50 eqid ⊢ ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) )
51 50 8 3 2 coe1f ⊢ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 )
52 16 51 syl ⊢ ( 𝜑 → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐾 )
54 fznn0sub ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → ( 𝑥 − 𝑦 ) ∈ ℕ0 )
55 54 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝑥 − 𝑦 ) ∈ ℕ0 )
56 53 55 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ∈ 𝐾 )
57 2 10 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) ∈ 𝐾 ∧ ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ∈ 𝐾 ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ∈ 𝐾 )
58 42 49 56 57 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ∈ 𝐾 )
59 58 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) : ( 0 ... 𝑥 ) ⟶ 𝐾 )
60 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → 𝑅 ∈ Ring )
61 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → 𝐶 ∈ 𝐾 )
62 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → 𝐷 ∈ ℕ0 )
63 eldifi ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) → 𝑦 ∈ ( 0 ... 𝑥 ) )
64 63 54 syl ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) → ( 𝑥 − 𝑦 ) ∈ ℕ0 )
65 64 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → ( 𝑥 − 𝑦 ) ∈ ℕ0 )
66 eldifsn ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ↔ ( 𝑦 ∈ ( 0 ... 𝑥 ) ∧ 𝑦 ≠ ( 𝑥 − 𝐷 ) ) )
67 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑥 ∈ ℕ0 )
68 67 nn0cnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑥 ∈ ℂ )
69 47 nn0cnd ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℂ )
70 69 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ∈ ℂ )
71 68 70 nncand ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝑥 − ( 𝑥 − 𝑦 ) ) = 𝑦 )
72 71 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 = ( 𝑥 − ( 𝑥 − 𝑦 ) ) )
73 oveq2 ⊢ ( 𝐷 = ( 𝑥 − 𝑦 ) → ( 𝑥 − 𝐷 ) = ( 𝑥 − ( 𝑥 − 𝑦 ) ) )
74 73 eqeq2d ⊢ ( 𝐷 = ( 𝑥 − 𝑦 ) → ( 𝑦 = ( 𝑥 − 𝐷 ) ↔ 𝑦 = ( 𝑥 − ( 𝑥 − 𝑦 ) ) ) )
75 72 74 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝐷 = ( 𝑥 − 𝑦 ) → 𝑦 = ( 𝑥 − 𝐷 ) ) )
76 75 necon3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝑦 ≠ ( 𝑥 − 𝐷 ) → 𝐷 ≠ ( 𝑥 − 𝑦 ) ) )
77 76 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ( 0 ... 𝑥 ) ∧ 𝑦 ≠ ( 𝑥 − 𝐷 ) ) ) → 𝐷 ≠ ( 𝑥 − 𝑦 ) )
78 66 77 sylan2b ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → 𝐷 ≠ ( 𝑥 − 𝑦 ) )
79 1 2 3 4 5 6 7 60 61 62 65 78 coe1tmfv2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) = 0 )
80 79 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × 0 ) )
81 2 10 1 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) ∈ 𝐾 ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
82 42 49 81 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
83 63 82 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
84 80 83 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥 − 𝐷 ) } ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
85 84 25 suppss2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) supp 0 ) ⊆ { ( 𝑥 − 𝐷 ) } )
86 2 1 23 25 41 59 85 gsumpt ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ ( 𝑥 − 𝐷 ) ) )
87 fveq2 ⊢ ( 𝑦 = ( 𝑥 − 𝐷 ) → ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) = ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) )
88 oveq2 ⊢ ( 𝑦 = ( 𝑥 − 𝐷 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 − ( 𝑥 − 𝐷 ) ) )
89 88 fveq2d ⊢ ( 𝑦 = ( 𝑥 − 𝐷 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) = ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) )
90 87 89 oveq12d ⊢ ( 𝑦 = ( 𝑥 − 𝐷 ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) ) )
91 eqid ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) )
92 ovex ⊢ ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) ) ∈ V
93 90 91 92 fvmpt ⊢ ( ( 𝑥 − 𝐷 ) ∈ ( 0 ... 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ ( 𝑥 − 𝐷 ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) ) )
94 41 93 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ‘ ( 𝑥 − 𝐷 ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) ) )
95 28 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
96 27 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐷 ∈ ℂ )
97 95 96 nncand ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 − ( 𝑥 − 𝐷 ) ) = 𝐷 )
98 97 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) = ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) )
99 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐶 ∈ 𝐾 )
100 1 2 3 4 5 6 7 coe1tmfv1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
101 21 99 27 100 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
102 98 101 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) = 𝐶 )
103 102 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥 − 𝐷 ) ) ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) )
104 86 94 103 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) )
105 104 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) )
106 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑅 ∈ Ring )
107 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐶 ∈ 𝐾 )
108 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐷 ∈ ℕ0 )
109 54 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥 − 𝑦 ) ∈ ℕ0 )
110 54 nn0red ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → ( 𝑥 − 𝑦 ) ∈ ℝ )
111 110 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥 − 𝑦 ) ∈ ℝ )
112 33 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑥 ∈ ℝ )
113 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐷 ∈ ℝ )
114 47 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑦 ∈ ℕ0 )
115 114 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 0 ≤ 𝑦 )
116 47 nn0red ⊢ ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℝ )
117 116 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑦 ∈ ℝ )
118 112 117 subge02d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 0 ≤ 𝑦 ↔ ( 𝑥 − 𝑦 ) ≤ 𝑥 ) )
119 115 118 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥 − 𝑦 ) ≤ 𝑥 )
120 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ¬ 𝐷 ≤ 𝑥 )
121 112 113 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥 < 𝐷 ↔ ¬ 𝐷 ≤ 𝑥 ) )
122 120 121 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑥 < 𝐷 )
123 111 112 113 119 122 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥 − 𝑦 ) < 𝐷 )
124 111 123 gtned ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐷 ≠ ( 𝑥 − 𝑦 ) )
125 1 2 3 4 5 6 7 106 107 108 109 124 coe1tmfv2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) = 0 )
126 125 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × 0 ) )
127 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( coe1 ‘ 𝐴 ) : ℕ0 ⟶ 𝐾 )
128 127 114 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) ∈ 𝐾 )
129 106 128 81 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
130 126 129 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷 ≤ 𝑥 ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
131 130 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) = 0 )
132 131 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) )
133 132 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) )
134 12 22 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
135 1 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑥 ) ∈ V ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
136 134 24 135 sylancl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
137 136 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
138 133 137 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷 ≤ 𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = 0 )
139 19 20 105 138 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) )
140 139 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) )
141 18 140 eqtrd ⊢ ( 𝜑 → ( coe1 ‘ ( 𝐴 ∙ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) )