Metamath Proof Explorer

Theorem coeaddlem

Description: Lemma for coeadd and dgradd . (Contributed by Mario Carneiro, 24-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
3 coeadd.3 ⊢ 𝑀 = ( deg ‘ 𝐹 )
4 coeadd.4 ⊢ 𝑁 = ( deg ‘ 𝐺 )
5 plyaddcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( Poly ‘ ℂ ) )
6 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
7 4 6 eqeltrid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
8 7 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
9 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
10 3 9 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
11 10 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℕ0 )
12 8 11 ifcld ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
13 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
14 13 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
15 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
16 15 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
17 2 coef3 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐵 : ℕ0 ⟶ ℂ )
18 17 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 : ℕ0 ⟶ ℂ )
19 nn0ex ⊢ ℕ0 ∈ V
20 19 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ℕ0 ∈ V )
21 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
22 14 16 18 20 20 21 off ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 ∘f + 𝐵 ) : ℕ0 ⟶ ℂ )
23 oveq12 ⊢ ( ( ( 𝐴 ‘ 𝑘 ) = 0 ∧ ( 𝐵 ‘ 𝑘 ) = 0 ) → ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) = ( 0 + 0 ) )
24 00id ⊢ ( 0 + 0 ) = 0
25 23 24 eqtrdi ⊢ ( ( ( 𝐴 ‘ 𝑘 ) = 0 ∧ ( 𝐵 ‘ 𝑘 ) = 0 ) → ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) = 0 )
26 16 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 Fn ℕ0 )
27 18 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 Fn ℕ0 )
28 eqidd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
29 eqidd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
30 26 27 20 20 21 28 29 ofval ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) )
31 30 eqeq1d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) = 0 ) )
32 25 31 syl5ibr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ‘ 𝑘 ) = 0 ∧ ( 𝐵 ‘ 𝑘 ) = 0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = 0 ) )
33 32 necon3ad ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → ¬ ( ( 𝐴 ‘ 𝑘 ) = 0 ∧ ( 𝐵 ‘ 𝑘 ) = 0 ) ) )
34 neorian ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ≠ 0 ∨ ( 𝐵 ‘ 𝑘 ) ≠ 0 ) ↔ ¬ ( ( 𝐴 ‘ 𝑘 ) = 0 ∧ ( 𝐵 ‘ 𝑘 ) = 0 ) )
35 33 34 syl6ibr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 ∨ ( 𝐵 ‘ 𝑘 ) ≠ 0 ) ) )
36 1 3 dgrub2 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
37 36 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
38 plyco0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) ) )
39 11 16 38 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) ) )
40 37 39 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
41 40 r19.21bi ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
42 11 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
43 42 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
44 8 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
45 44 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
46 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
47 43 45 46 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
48 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
49 48 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
50 12 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
51 50 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℝ )
52 letr ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℝ ) → ( ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
53 49 43 51 52 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
54 47 53 mpan2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ≤ 𝑀 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
55 41 54 syld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
56 2 4 dgrub2 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
57 56 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
58 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 : ℕ0 ⟶ ℂ ) → ( ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
59 8 18 58 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
60 57 59 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
61 60 r19.21bi ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
62 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
63 43 45 62 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
64 letr ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℝ ) → ( ( 𝑘 ≤ 𝑁 ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
65 49 45 51 64 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑁 ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
66 63 65 mpan2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ≤ 𝑁 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
67 61 66 syld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
68 55 67 jaod ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ‘ 𝑘 ) ≠ 0 ∨ ( 𝐵 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
69 35 68 syld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
70 69 ralrimiva ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
71 plyco0 ⊢ ( ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 ∧ ( 𝐴 ∘f + 𝐵 ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝐴 ∘f + 𝐵 ) “ ( ℤ≥ ‘ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) )
72 12 22 71 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( 𝐴 ∘f + 𝐵 ) “ ( ℤ≥ ‘ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) )
73 70 72 mpbird ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴 ∘f + 𝐵 ) “ ( ℤ≥ ‘ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) + 1 ) ) ) = { 0 } )
74 simpl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
75 simpr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
76 1 3 coeid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
77 76 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
78 2 4 coeid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
79 78 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
80 74 75 11 8 16 18 37 57 77 79 plyaddlem1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
81 5 12 22 73 80 coeeq ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) )
82 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ∈ ℕ0 )
83 ffvelrn ⊢ ( ( ( 𝐴 ∘f + 𝐵 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
84 22 82 83 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
85 5 12 84 80 dgrle ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
86 81 85 jca ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) ∧ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )