Metamath Proof Explorer

Theorem iprodmul

Description: Multiplication of infinite sums. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses iprodmul.1 ⊢ Z = ℤ ≥ M
iprodmul.2 ⊢ φ → M ∈ ℤ
iprodmul.3 ⊢ φ → ∃ n ∈ Z ∃ y y ≠ 0 ∧ seq n × F ⇝ y
iprodmul.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
iprodmul.5 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
iprodmul.6 ⊢ φ → ∃ m ∈ Z ∃ z z ≠ 0 ∧ seq m × G ⇝ z
iprodmul.7 ⊢ φ ∧ k ∈ Z → G ⁡ k = B
iprodmul.8 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
Assertion iprodmul ⊢ φ → ∏ k ∈ Z A ⁢ B = ∏ k ∈ Z A ⁢ ∏ k ∈ Z B

Proof

Step Hyp Ref Expression
1 iprodmul.1 ⊢ Z = ℤ ≥ M
2 iprodmul.2 ⊢ φ → M ∈ ℤ
3 iprodmul.3 ⊢ φ → ∃ n ∈ Z ∃ y y ≠ 0 ∧ seq n × F ⇝ y
4 iprodmul.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
5 iprodmul.5 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
6 iprodmul.6 ⊢ φ → ∃ m ∈ Z ∃ z z ≠ 0 ∧ seq m × G ⇝ z
7 iprodmul.7 ⊢ φ ∧ k ∈ Z → G ⁡ k = B
8 iprodmul.8 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
9 4 5 eqeltrd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
10 7 8 eqeltrd ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ
11 fveq2 ⊢ a = k → F ⁡ a = F ⁡ k
12 fveq2 ⊢ a = k → G ⁡ a = G ⁡ k
13 11 12 oveq12d ⊢ a = k → F ⁡ a ⁢ G ⁡ a = F ⁡ k ⁢ G ⁡ k
14 eqid ⊢ a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a = a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a
15 ovex ⊢ F ⁡ k ⁢ G ⁡ k ∈ V
16 13 14 15 fvmpt ⊢ k ∈ Z → a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⁡ k = F ⁡ k ⁢ G ⁡ k
17 16 adantl ⊢ φ ∧ k ∈ Z → a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⁡ k = F ⁡ k ⁢ G ⁡ k
18 1 3 9 6 10 17 ntrivcvgmul ⊢ φ → ∃ p ∈ Z ∃ w w ≠ 0 ∧ seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⇝ w
19 fveq2 ⊢ m = a → F ⁡ m = F ⁡ a
20 fveq2 ⊢ m = a → G ⁡ m = G ⁡ a
21 19 20 oveq12d ⊢ m = a → F ⁡ m ⁢ G ⁡ m = F ⁡ a ⁢ G ⁡ a
22 21 cbvmptv ⊢ m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m = a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a
23 seqeq3 ⊢ m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m = a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a → seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m = seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a
24 22 23 ax-mp ⊢ seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m = seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a
25 24 breq1i ⊢ seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⇝ w ↔ seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⇝ w
26 25 anbi2i ⊢ w ≠ 0 ∧ seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⇝ w ↔ w ≠ 0 ∧ seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⇝ w
27 26 exbii ⊢ ∃ w w ≠ 0 ∧ seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⇝ w ↔ ∃ w w ≠ 0 ∧ seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⇝ w
28 27 rexbii ⊢ ∃ p ∈ Z ∃ w w ≠ 0 ∧ seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⇝ w ↔ ∃ p ∈ Z ∃ w w ≠ 0 ∧ seq p × a ∈ Z ⟼ F ⁡ a ⁢ G ⁡ a ⇝ w
29 18 28 sylibr ⊢ φ → ∃ p ∈ Z ∃ w w ≠ 0 ∧ seq p × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⇝ w
30 eqid ⊢ m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m = m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m
31 fveq2 ⊢ m = k → F ⁡ m = F ⁡ k
32 fveq2 ⊢ m = k → G ⁡ m = G ⁡ k
33 31 32 oveq12d ⊢ m = k → F ⁡ m ⁢ G ⁡ m = F ⁡ k ⁢ G ⁡ k
34 simpr ⊢ φ ∧ k ∈ Z → k ∈ Z
35 9 10 mulcld ⊢ φ ∧ k ∈ Z → F ⁡ k ⁢ G ⁡ k ∈ ℂ
36 30 33 34 35 fvmptd3 ⊢ φ ∧ k ∈ Z → m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⁡ k = F ⁡ k ⁢ G ⁡ k
37 4 7 oveq12d ⊢ φ ∧ k ∈ Z → F ⁡ k ⁢ G ⁡ k = A ⁢ B
38 36 37 eqtrd ⊢ φ ∧ k ∈ Z → m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⁡ k = A ⁢ B
39 5 8 mulcld ⊢ φ ∧ k ∈ Z → A ⁢ B ∈ ℂ
40 1 2 3 4 5 iprodclim2 ⊢ φ → seq M × F ⇝ ∏ k ∈ Z A
41 seqex ⊢ seq M × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ∈ V
42 41 a1i ⊢ φ → seq M × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ∈ V
43 1 2 6 7 8 iprodclim2 ⊢ φ → seq M × G ⇝ ∏ k ∈ Z B
44 1 2 9 prodf ⊢ φ → seq M × F : Z ⟶ ℂ
45 44 ffvelcdmda ⊢ φ ∧ j ∈ Z → seq M × F ⁡ j ∈ ℂ
46 1 2 10 prodf ⊢ φ → seq M × G : Z ⟶ ℂ
47 46 ffvelcdmda ⊢ φ ∧ j ∈ Z → seq M × G ⁡ j ∈ ℂ
48 simpr ⊢ φ ∧ j ∈ Z → j ∈ Z
49 48 1 eleqtrdi ⊢ φ ∧ j ∈ Z → j ∈ ℤ ≥ M
50 elfzuz ⊢ k ∈ M … j → k ∈ ℤ ≥ M
51 50 1 eleqtrrdi ⊢ k ∈ M … j → k ∈ Z
52 51 9 sylan2 ⊢ φ ∧ k ∈ M … j → F ⁡ k ∈ ℂ
53 52 adantlr ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → F ⁡ k ∈ ℂ
54 51 10 sylan2 ⊢ φ ∧ k ∈ M … j → G ⁡ k ∈ ℂ
55 54 adantlr ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → G ⁡ k ∈ ℂ
56 36 adantlr ⊢ φ ∧ j ∈ Z ∧ k ∈ Z → m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⁡ k = F ⁡ k ⁢ G ⁡ k
57 51 56 sylan2 ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⁡ k = F ⁡ k ⁢ G ⁡ k
58 49 53 55 57 prodfmul ⊢ φ ∧ j ∈ Z → seq M × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⁡ j = seq M × F ⁡ j ⁢ seq M × G ⁡ j
59 1 2 40 42 43 45 47 58 climmul ⊢ φ → seq M × m ∈ Z ⟼ F ⁡ m ⁢ G ⁡ m ⇝ ∏ k ∈ Z A ⁢ ∏ k ∈ Z B
60 1 2 29 38 39 59 iprodclim ⊢ φ → ∏ k ∈ Z A ⁢ B = ∏ k ∈ Z A ⁢ ∏ k ∈ Z B