Metamath Proof Explorer

Theorem plymullem

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

Ref Expression
Hypotheses plyadd.1 ⊢ φ → F ∈ Poly ⁡ S
plyadd.2 ⊢ φ → G ∈ Poly ⁡ S
plyadd.3 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
plyadd.m ⊢ φ → M ∈ ℕ 0
plyadd.n ⊢ φ → N ∈ ℕ 0
plyadd.a ⊢ φ → A ∈ S ∪ 0 ℕ 0
plyadd.b ⊢ φ → B ∈ S ∪ 0 ℕ 0
plyadd.a2 ⊢ φ → A ℤ ≥ M + 1 = 0
plyadd.b2 ⊢ φ → B ℤ ≥ N + 1 = 0
plyadd.f ⊢ φ → F = z ∈ ℂ ⟼ ∑ k = 0 M A ⁡ k ⁢ z k
plyadd.g ⊢ φ → G = z ∈ ℂ ⟼ ∑ k = 0 N B ⁡ k ⁢ z k
plymul.x ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
Assertion plymullem ⊢ φ → F × f G ∈ Poly ⁡ S

Proof

Step Hyp Ref Expression
1 plyadd.1 ⊢ φ → F ∈ Poly ⁡ S
2 plyadd.2 ⊢ φ → G ∈ Poly ⁡ S
3 plyadd.3 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
4 plyadd.m ⊢ φ → M ∈ ℕ 0
5 plyadd.n ⊢ φ → N ∈ ℕ 0
6 plyadd.a ⊢ φ → A ∈ S ∪ 0 ℕ 0
7 plyadd.b ⊢ φ → B ∈ S ∪ 0 ℕ 0
8 plyadd.a2 ⊢ φ → A ℤ ≥ M + 1 = 0
9 plyadd.b2 ⊢ φ → B ℤ ≥ N + 1 = 0
10 plyadd.f ⊢ φ → F = z ∈ ℂ ⟼ ∑ k = 0 M A ⁡ k ⁢ z k
11 plyadd.g ⊢ φ → G = z ∈ ℂ ⟼ ∑ k = 0 N B ⁡ k ⁢ z k
12 plymul.x ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
13 plybss ⊢ F ∈ Poly ⁡ S → S ⊆ ℂ
14 1 13 syl ⊢ φ → S ⊆ ℂ
15 0cnd ⊢ φ → 0 ∈ ℂ
16 15 snssd ⊢ φ → 0 ⊆ ℂ
17 14 16 unssd ⊢ φ → S ∪ 0 ⊆ ℂ
18 cnex ⊢ ℂ ∈ V
19 ssexg ⊢ S ∪ 0 ⊆ ℂ ∧ ℂ ∈ V → S ∪ 0 ∈ V
20 17 18 19 sylancl ⊢ φ → S ∪ 0 ∈ V
21 nn0ex ⊢ ℕ 0 ∈ V
22 elmapg ⊢ S ∪ 0 ∈ V ∧ ℕ 0 ∈ V → A ∈ S ∪ 0 ℕ 0 ↔ A : ℕ 0 ⟶ S ∪ 0
23 20 21 22 sylancl ⊢ φ → A ∈ S ∪ 0 ℕ 0 ↔ A : ℕ 0 ⟶ S ∪ 0
24 6 23 mpbid ⊢ φ → A : ℕ 0 ⟶ S ∪ 0
25 24 17 fssd ⊢ φ → A : ℕ 0 ⟶ ℂ
26 elmapg ⊢ S ∪ 0 ∈ V ∧ ℕ 0 ∈ V → B ∈ S ∪ 0 ℕ 0 ↔ B : ℕ 0 ⟶ S ∪ 0
27 20 21 26 sylancl ⊢ φ → B ∈ S ∪ 0 ℕ 0 ↔ B : ℕ 0 ⟶ S ∪ 0
28 7 27 mpbid ⊢ φ → B : ℕ 0 ⟶ S ∪ 0
29 28 17 fssd ⊢ φ → B : ℕ 0 ⟶ ℂ
30 1 2 4 5 25 29 8 9 10 11 plymullem1 ⊢ φ → F × f G = z ∈ ℂ ⟼ ∑ n = 0 M + N ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ⁢ z n
31 4 5 nn0addcld ⊢ φ → M + N ∈ ℕ 0
32 eqid ⊢ S ∪ 0 = S ∪ 0
33 14 32 3 un0addcl ⊢ φ ∧ x ∈ S ∪ 0 ∧ y ∈ S ∪ 0 → x + y ∈ S ∪ 0
34 fzfid ⊢ φ → 0 … n ∈ Fin
35 elfznn0 ⊢ k ∈ 0 … n → k ∈ ℕ 0
36 ffvelcdm ⊢ A : ℕ 0 ⟶ S ∪ 0 ∧ k ∈ ℕ 0 → A ⁡ k ∈ S ∪ 0
37 24 35 36 syl2an ⊢ φ ∧ k ∈ 0 … n → A ⁡ k ∈ S ∪ 0
38 fznn0sub ⊢ k ∈ 0 … n → n − k ∈ ℕ 0
39 ffvelcdm ⊢ B : ℕ 0 ⟶ S ∪ 0 ∧ n − k ∈ ℕ 0 → B ⁡ n − k ∈ S ∪ 0
40 28 38 39 syl2an ⊢ φ ∧ k ∈ 0 … n → B ⁡ n − k ∈ S ∪ 0
41 37 40 jca ⊢ φ ∧ k ∈ 0 … n → A ⁡ k ∈ S ∪ 0 ∧ B ⁡ n − k ∈ S ∪ 0
42 14 32 12 un0mulcl ⊢ φ ∧ x ∈ S ∪ 0 ∧ y ∈ S ∪ 0 → x ⁢ y ∈ S ∪ 0
43 42 caovclg ⊢ φ ∧ A ⁡ k ∈ S ∪ 0 ∧ B ⁡ n − k ∈ S ∪ 0 → A ⁡ k ⁢ B ⁡ n − k ∈ S ∪ 0
44 41 43 syldan ⊢ φ ∧ k ∈ 0 … n → A ⁡ k ⁢ B ⁡ n − k ∈ S ∪ 0
45 ssun2 ⊢ 0 ⊆ S ∪ 0
46 c0ex ⊢ 0 ∈ V
47 46 snss ⊢ 0 ∈ S ∪ 0 ↔ 0 ⊆ S ∪ 0
48 45 47 mpbir ⊢ 0 ∈ S ∪ 0
49 48 a1i ⊢ φ → 0 ∈ S ∪ 0
50 17 33 34 44 49 fsumcllem ⊢ φ → ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ∈ S ∪ 0
51 50 adantr ⊢ φ ∧ n ∈ 0 … M + N → ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ∈ S ∪ 0
52 17 31 51 elplyd ⊢ φ → z ∈ ℂ ⟼ ∑ n = 0 M + N ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ⁢ z n ∈ Poly ⁡ S ∪ 0
53 30 52 eqeltrd ⊢ φ → F × f G ∈ Poly ⁡ S ∪ 0
54 plyun0 ⊢ Poly ⁡ S ∪ 0 = Poly ⁡ S
55 53 54 eleqtrdi ⊢ φ → F × f G ∈ Poly ⁡ S