Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ( 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 ffvelrn ⊢ ( ( ( 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 ‘ 𝐹 ) ) )