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 ) ) )