Metamath Proof Explorer

Theorem coemulhi

Description: The leading coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
coemulhi.3 ⊢ 𝑀 = ( deg ‘ 𝐹 )
coemulhi.4 ⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion coemulhi ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
3 coemulhi.3 ⊢ 𝑀 = ( deg ‘ 𝐹 )
4 coemulhi.4 ⊢ 𝑁 = ( deg ‘ 𝐺 )
5 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
6 3 5 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
7 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
8 4 7 eqeltrid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
9 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
10 6 8 9 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
11 1 2 coemul ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
12 10 11 mpd3an3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
13 8 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
14 13 nn0ge0d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 0 ≤ 𝑁 )
15 6 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℕ0 )
16 15 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℝ )
17 13 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℝ )
18 16 17 addge01d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 0 ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
19 14 18 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
20 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
21 15 20 eleqtrdi ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
22 10 nn0zd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
23 elfz5 ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
24 21 22 23 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
25 19 24 mpbird ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
26 25 snssd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → { 𝑀 } ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
27 elsni ⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
28 27 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → 𝑘 = 𝑀 )
29 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑀 ) )
30 oveq2 ⊢ ( 𝑘 = 𝑀 → ( ( 𝑀 + 𝑁 ) − 𝑘 ) = ( ( 𝑀 + 𝑁 ) − 𝑀 ) )
31 30 fveq2d ⊢ ( 𝑘 = 𝑀 → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) )
32 29 31 oveq12d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
33 28 32 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
34 16 recnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℂ )
35 17 recnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℂ )
36 34 35 pncan2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
37 36 fveq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝐵 ‘ 𝑁 ) )
38 37 oveq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ 𝑁 ) ) )
39 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
40 39 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
41 40 15 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
42 2 coef3 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐵 : ℕ0 ⟶ ℂ )
43 42 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 : ℕ0 ⟶ ℂ )
44 43 13 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵 ‘ 𝑁 ) ∈ ℂ )
45 41 44 mulcld ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ 𝑁 ) ) ∈ ℂ )
46 38 45 eqeltrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) ∈ ℂ )
47 46 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) ∈ ℂ )
48 33 47 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ { 𝑀 } ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) ∈ ℂ )
49 simpl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
50 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
51 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑘 ∈ ℕ0 )
52 50 51 syl ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → 𝑘 ∈ ℕ0 )
53 1 3 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑀 )
54 53 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
55 49 52 54 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
56 55 necon1bd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ 𝑘 ≤ 𝑀 → ( 𝐴 ‘ 𝑘 ) = 0 ) )
57 56 imp ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 𝐴 ‘ 𝑘 ) = 0 )
58 57 oveq1d ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( 0 · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
59 43 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → 𝐵 : ℕ0 ⟶ ℂ )
60 50 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
61 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 )
62 60 61 syl ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 )
63 59 62 ffvelcdmd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∈ ℂ )
64 63 mul02d ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 0 · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
65 58 64 eqtrd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
66 16 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑀 ∈ ℝ )
67 50 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
68 67 51 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ∈ ℕ0 )
69 68 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ∈ ℝ )
70 17 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑁 ∈ ℝ )
71 66 69 70 leadd1d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀 ≤ 𝑘 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝑘 + 𝑁 ) ) )
72 10 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
73 72 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
74 73 69 70 lesubadd2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝑘 + 𝑁 ) ) )
75 71 74 bitr4d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑀 ≤ 𝑘 ↔ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
76 75 notbid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ 𝑀 ≤ 𝑘 ↔ ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
77 76 biimpa ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 )
78 simpr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
79 50 61 syl ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 )
80 2 4 dgrub ⊢ ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 ∧ ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ≠ 0 ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 )
81 80 3expia ⊢ ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ℕ0 ) → ( ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ≠ 0 → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
82 78 79 81 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ≠ 0 → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) )
83 82 necon1bd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = 0 ) )
84 83 imp ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ≤ 𝑁 ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = 0 )
85 77 84 syldan ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) = 0 )
86 85 oveq2d ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · 0 ) )
87 40 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → 𝐴 : ℕ0 ⟶ ℂ )
88 52 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → 𝑘 ∈ ℕ0 )
89 87 88 ffvelcdmd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
90 89 mul01d ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
91 86 90 eqtrd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) ∧ ¬ 𝑀 ≤ 𝑘 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
92 eldifsni ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) → 𝑘 ≠ 𝑀 )
93 92 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → 𝑘 ≠ 𝑀 )
94 69 66 letri3d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑘 = 𝑀 ↔ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘 ) ) )
95 94 necon3abid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( 𝑘 ≠ 𝑀 ↔ ¬ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘 ) ) )
96 93 95 mpbid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ¬ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘 ) )
97 ianor ⊢ ( ¬ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘 ) ↔ ( ¬ 𝑘 ≤ 𝑀 ∨ ¬ 𝑀 ≤ 𝑘 ) )
98 96 97 sylib ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ¬ 𝑘 ≤ 𝑀 ∨ ¬ 𝑀 ≤ 𝑘 ) )
99 65 91 98 mpjaodan ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ { 𝑀 } ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = 0 )
100 fzfid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 0 ... ( 𝑀 + 𝑁 ) ) ∈ Fin )
101 26 48 99 100 fsumss ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) )
102 32 sumsn ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
103 15 46 102 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ) )
104 103 38 eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑘 ∈ { 𝑀 } ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ 𝑁 ) ) )
105 12 101 104 3eqtr2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( 𝐵 ‘ 𝑁 ) ) )