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 = ( 0_g ‘ 𝑅 )
	coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1tm.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1tm.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	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	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
Assertion	coe1tmmul	⊢ ( 𝜑 → ( coe₁ ‘ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∙ 𝐴 ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝐷 ≤ 𝑥 , ( 𝐶 × ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )

Proof

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

Metamath Proof Explorer

Theorem coe1tmmul

Proof