Theorem coemulc

Description: The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Assertion	coemulc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( ℕ0 × { 𝐴 } ) ∘f · ( coeff ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℂ ⊆ ℂ
2		plyconst	⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
4		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
5	4	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
6		plymulcl	⊢ ( ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ∈ ( Poly ‘ ℂ ) ) → ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ∈ ( Poly ‘ ℂ ) )
7	3 5 6	syl2an	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ∈ ( Poly ‘ ℂ ) )
8		eqid	⊢ ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) )
9	8	coef3	⊢ ( ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ∈ ( Poly ‘ ℂ ) → ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) : ℕ0 ⟶ ℂ )
10		ffn	⊢ ( ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) : ℕ0 ⟶ ℂ → ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) Fn ℕ0 )
11	7 9 10	3syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) Fn ℕ0 )
12		fconstg	⊢ ( 𝐴 ∈ ℂ → ( ℕ0 × { 𝐴 } ) : ℕ0 ⟶ { 𝐴 } )
13	12	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℕ0 × { 𝐴 } ) : ℕ0 ⟶ { 𝐴 } )
14	13	ffnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℕ0 × { 𝐴 } ) Fn ℕ0 )
15		eqid	⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
16	15	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
17	16	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
18	17	ffnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ 𝐹 ) Fn ℕ0 )
19		nn0ex	⊢ ℕ0 ∈ V
20	19	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ℕ0 ∈ V )
21		inidm	⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
22	14 18 20 20 21	offn	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℕ0 × { 𝐴 } ) ∘f · ( coeff ‘ 𝐹 ) ) Fn ℕ0 )
23	3	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
24		eqid	⊢ ( coeff ‘ ( ℂ × { 𝐴 } ) ) = ( coeff ‘ ( ℂ × { 𝐴 } ) )
25	24	coefv0	⊢ ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) )
26	23 25	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) )
27		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
28		0cn	⊢ 0 ∈ ℂ
29		fvconst2g	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
30	27 28 29	sylancl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
31	26 30	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) = 𝐴 )
32		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
33	32	nn0cnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
34	33	subid1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 − 0 ) = 𝑛 )
35	34	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) = ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) )
36	31 35	oveq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) = ( 𝐴 · ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) ) )
37	5	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
38	24 15	coemul	⊢ ( ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) )
39	23 37 32 38	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) )
40		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
41	32 40	eleqtrdi	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ( ℤ≥ ‘ 0 ) )
42		fzss2	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 0 ) ⊆ ( 0 ... 𝑛 ) )
43	41 42	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ... 0 ) ⊆ ( 0 ... 𝑛 ) )
44		elfz1eq	⊢ ( 𝑘 ∈ ( 0 ... 0 ) → 𝑘 = 0 )
45	44	adantl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → 𝑘 = 0 )
46		fveq2	⊢ ( 𝑘 = 0 → ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) = ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) )
47		oveq2	⊢ ( 𝑘 = 0 → ( 𝑛 − 𝑘 ) = ( 𝑛 − 0 ) )
48	47	fveq2d	⊢ ( 𝑘 = 0 → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) )
49	46 48	oveq12d	⊢ ( 𝑘 = 0 → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) )
50	45 49	syl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) )
51	17	ffvelcdmda	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
52	27 51	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 · ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) ) ∈ ℂ )
53	36 52	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) ∈ ℂ )
54	53	adantr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) ∈ ℂ )
55	50 54	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ℂ )
56		eldifn	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) → ¬ 𝑘 ∈ ( 0 ... 0 ) )
57	56	adantl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 0 ) )
58		eldifi	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ( 0 ... 𝑛 ) )
59		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
60	58 59	syl	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ℕ0 )
61		eqid	⊢ ( deg ‘ ( ℂ × { 𝐴 } ) ) = ( deg ‘ ( ℂ × { 𝐴 } ) )
62	24 61	dgrub	⊢ ( ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ 𝑘 ∈ ℕ0 ∧ ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ ( deg ‘ ( ℂ × { 𝐴 } ) ) )
63	62	3expia	⊢ ( ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( deg ‘ ( ℂ × { 𝐴 } ) ) ) )
64	23 60 63	syl2an	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( deg ‘ ( ℂ × { 𝐴 } ) ) ) )
65		0dgr	⊢ ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )
66	65	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )
67	66	breq2d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( 𝑘 ≤ ( deg ‘ ( ℂ × { 𝐴 } ) ) ↔ 𝑘 ≤ 0 ) )
68	60	adantl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → 𝑘 ∈ ℕ0 )
69		nn0le0eq0	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 ≤ 0 ↔ 𝑘 = 0 ) )
70	68 69	syl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( 𝑘 ≤ 0 ↔ 𝑘 = 0 ) )
71	67 70	bitrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( 𝑘 ≤ ( deg ‘ ( ℂ × { 𝐴 } ) ) ↔ 𝑘 = 0 ) )
72	64 71	sylibd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 = 0 ) )
73		id	⊢ ( 𝑘 = 0 → 𝑘 = 0 )
74		0z	⊢ 0 ∈ ℤ
75		elfz3	⊢ ( 0 ∈ ℤ → 0 ∈ ( 0 ... 0 ) )
76	74 75	ax-mp	⊢ 0 ∈ ( 0 ... 0 )
77	73 76	eqeltrdi	⊢ ( 𝑘 = 0 → 𝑘 ∈ ( 0 ... 0 ) )
78	72 77	syl6	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 0 ) ) )
79	78	necon1bd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 0 ) → ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) = 0 ) )
80	57 79	mpd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) = 0 )
81	80	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) )
82	17	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
83		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑘 ) ∈ ℕ0 )
84	58 83	syl	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) → ( 𝑛 − 𝑘 ) ∈ ℕ0 )
85		ffvelcdm	⊢ ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ∧ ( 𝑛 − 𝑘 ) ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ∈ ℂ )
86	82 84 85	syl2an	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ∈ ℂ )
87	86	mul02d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
88	81 87	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑛 ) ∖ ( 0 ... 0 ) ) ) → ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
89		fzfid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ... 𝑛 ) ∈ Fin )
90	43 55 88 89	fsumss	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) )
91	49	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) )
92	74 53 91	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) )
93	39 90 92	3eqtr2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝑛 ) = ( ( ( coeff ‘ ( ℂ × { 𝐴 } ) ) ‘ 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 0 ) ) ) )
94		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 ∈ ℂ )
95		eqidd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) )
96	20 94 18 95	ofc1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℕ0 × { 𝐴 } ) ∘f · ( coeff ‘ 𝐹 ) ) ‘ 𝑛 ) = ( 𝐴 · ( ( coeff ‘ 𝐹 ) ‘ 𝑛 ) ) )
97	36 93 96	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝑛 ) = ( ( ( ℕ0 × { 𝐴 } ) ∘f · ( coeff ‘ 𝐹 ) ) ‘ 𝑛 ) )
98	11 22 97	eqfnfvd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( ℕ0 × { 𝐴 } ) ∘f · ( coeff ‘ 𝐹 ) ) )