iprodmul

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

	Ref	Expression
Hypotheses	iprodmul.1	$⊢ Z = ℤ_{\geq M}$
	iprodmul.2	$⊢ φ \to M \in ℤ$
	iprodmul.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
	iprodmul.4	$⊢ (φ \land k \in Z) \to F (k) = A$
	iprodmul.5	$⊢ (φ \land k \in Z) \to A \in ℂ$
	iprodmul.6	$⊢ φ \to \exists m \in Z \exists z (z \neq 0 \land seq m (\times G) ⇝ z)$
	iprodmul.7	$⊢ (φ \land k \in Z) \to G (k) = B$
	iprodmul.8	$⊢ (φ \land k \in Z) \to B \in ℂ$
Assertion	iprodmul	$⊢ φ \to \prod_{k \in Z} A B = \prod_{k \in Z} A \prod_{k \in Z} B$

Proof

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

Metamath Proof Explorer

Theorem iprodmul

Proof