Metamath Proof Explorer

Theorem plymullem

Description: Lemma for plymul . (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plyadd.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plyadd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plyadd.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
plyadd.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
plyadd.a ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
plyadd.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
plyadd.a2 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
plyadd.b2 ⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
plyadd.f ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
plyadd.g ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
plymul.x ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
Assertion plymullem ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 plyadd.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 plyadd.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
3 plyadd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 plyadd.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 plyadd.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 plyadd.a ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
7 plyadd.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
8 plyadd.a2 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
9 plyadd.b2 ⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
10 plyadd.f ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
11 plyadd.g ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
12 plymul.x ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
13 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
14 1 13 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
15 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
16 15 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℂ )
17 14 16 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
18 cnex ⊢ ℂ ∈ V
19 ssexg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
20 17 18 19 sylancl ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ∈ V )
21 nn0ex ⊢ ℕ0 ∈ V
22 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
23 20 21 22 sylancl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
24 6 23 mpbid ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
25 24 17 fssd ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
26 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
27 20 21 26 sylancl ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
28 7 27 mpbid ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
29 28 17 fssd ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ )
30 1 2 4 5 25 29 8 9 10 11 plymullem1 ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑛 ) ) ) )
31 4 5 nn0addcld ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
32 eqid ⊢ ( 𝑆 ∪ { 0 } ) = ( 𝑆 ∪ { 0 } )
33 14 32 3 un0addcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∪ { 0 } ) ∧ 𝑦 ∈ ( 𝑆 ∪ { 0 } ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 𝑆 ∪ { 0 } ) )
34 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑛 ) ∈ Fin )
35 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
36 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
37 24 35 36 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
38 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑘 ) ∈ ℕ0 )
39 ffvelcdm ⊢ ( ( 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ( 𝑛 − 𝑘 ) ∈ ℕ0 ) → ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) )
40 28 38 39 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) )
41 37 40 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) ∧ ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) ) )
42 14 32 12 un0mulcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∪ { 0 } ) ∧ 𝑦 ∈ ( 𝑆 ∪ { 0 } ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝑆 ∪ { 0 } ) )
43 42 caovclg ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) ∧ ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ∈ ( 𝑆 ∪ { 0 } ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ( 𝑆 ∪ { 0 } ) )
44 41 43 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ( 𝑆 ∪ { 0 } ) )
45 ssun2 ⊢ { 0 } ⊆ ( 𝑆 ∪ { 0 } )
46 c0ex ⊢ 0 ∈ V
47 46 snss ⊢ ( 0 ∈ ( 𝑆 ∪ { 0 } ) ↔ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) )
48 45 47 mpbir ⊢ 0 ∈ ( 𝑆 ∪ { 0 } )
49 48 a1i ⊢ ( 𝜑 → 0 ∈ ( 𝑆 ∪ { 0 } ) )
50 17 33 34 44 49 fsumcllem ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ( 𝑆 ∪ { 0 } ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ( 𝑆 ∪ { 0 } ) )
52 17 31 51 elplyd ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑛 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
53 30 52 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
54 plyun0 ⊢ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )
55 53 54 eleqtrdi ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )