Theorem iprodmul

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

	Ref	Expression
Hypotheses	iprodmul.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iprodmul.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iprodmul.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
	iprodmul.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	iprodmul.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	iprodmul.6	⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) )
	iprodmul.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
	iprodmul.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
Assertion	iprodmul	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 ( 𝐴 · 𝐵 ) = ( ∏ 𝑘 ∈ 𝑍 𝐴 · ∏ 𝑘 ∈ 𝑍 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		iprodmul.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iprodmul.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iprodmul.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
4		iprodmul.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		iprodmul.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
6		iprodmul.6	⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) )
7		iprodmul.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
8		iprodmul.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
9	4 5	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
10	7 8	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
11		fveq2	⊢ ( 𝑎 = 𝑘 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑘 ) )
12		fveq2	⊢ ( 𝑎 = 𝑘 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ 𝑘 ) )
13	11 12	oveq12d	⊢ ( 𝑎 = 𝑘 → ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
14		eqid	⊢ ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) )
15		ovex	⊢ ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ∈ V
16	13 14 15	fvmpt	⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
18	1 3 9 6 10 17	ntrivcvgmul	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ) ⇝ 𝑤 ) )
19		fveq2	⊢ ( 𝑚 = 𝑎 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑎 ) )
20		fveq2	⊢ ( 𝑚 = 𝑎 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑎 ) )
21	19 20	oveq12d	⊢ ( 𝑚 = 𝑎 → ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) )
22	21	cbvmptv	⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) = ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) )
23		seqeq3	⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) = ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) → seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) = seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ) )
24	22 23	ax-mp	⊢ seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) = seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) )
25	24	breq1i	⊢ ( seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ 𝑤 ↔ seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ) ⇝ 𝑤 )
26	25	anbi2i	⊢ ( ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ 𝑤 ) ↔ ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ) ⇝ 𝑤 ) )
27	26	exbii	⊢ ( ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ 𝑤 ) ↔ ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ) ⇝ 𝑤 ) )
28	27	rexbii	⊢ ( ∃ 𝑝 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ 𝑤 ) ↔ ∃ 𝑝 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑎 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑎 ) · ( 𝐺 ‘ 𝑎 ) ) ) ) ⇝ 𝑤 ) )
29	18 28	sylibr	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ 𝑤 ) )
30		eqid	⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) )
31		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
32		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) )
33	31 32	oveq12d	⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
35	9 10	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
36	30 33 34 35	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
37	4 7	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 · 𝐵 ) )
38	36 37	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐴 · 𝐵 ) )
39	5 8	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
40	1 2 3 4 5	iprodclim2	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ∏ 𝑘 ∈ 𝑍 𝐴 )
41		seqex	⊢ seq 𝑀 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ V
42	41	a1i	⊢ ( 𝜑 → seq 𝑀 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ V )
43	1 2 6 7 8	iprodclim2	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐺 ) ⇝ ∏ 𝑘 ∈ 𝑍 𝐵 )
44	1 2 9	prodf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )
45	44	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
46	1 2 10	prodf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐺 ) : 𝑍 ⟶ ℂ )
47	46	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑗 ) ∈ ℂ )
48		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
49	48 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
50		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
51	50 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
52	51 9	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
53	52	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
54	51 10	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
55	54	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
56	36	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
57	51 56	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
58	49 53 55 57	prodfmul	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) · ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑗 ) ) )
59	1 2 40 42 43 45 47 58	climmul	⊢ ( 𝜑 → seq 𝑀 ( · , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) · ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ ( ∏ 𝑘 ∈ 𝑍 𝐴 · ∏ 𝑘 ∈ 𝑍 𝐵 ) )
60	1 2 29 38 39 59	iprodclim	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 ( 𝐴 · 𝐵 ) = ( ∏ 𝑘 ∈ 𝑍 𝐴 · ∏ 𝑘 ∈ 𝑍 𝐵 ) )