Metamath Proof Explorer


Theorem iprodclim3

Description: The sequence of partial finite product of a converging infinite product converge to the infinite product of the series. Note that j must not occur in A . (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses iprodclim3.1 Z = M
iprodclim3.2 φ M
iprodclim3.3 φ n Z y y 0 seq n × k Z A y
iprodclim3.4 φ F dom
iprodclim3.5 φ k Z A
iprodclim3.6 φ j Z F j = k = M j A
Assertion iprodclim3 φ F k Z A

Proof

Step Hyp Ref Expression
1 iprodclim3.1 Z = M
2 iprodclim3.2 φ M
3 iprodclim3.3 φ n Z y y 0 seq n × k Z A y
4 iprodclim3.4 φ F dom
5 iprodclim3.5 φ k Z A
6 iprodclim3.6 φ j Z F j = k = M j A
7 climdm F dom F F
8 4 7 sylib φ F F
9 prodfc m Z k Z A m = k Z A
10 eqidd φ m Z k Z A m = k Z A m
11 5 fmpttd φ k Z A : Z
12 11 ffvelrnda φ m Z k Z A m
13 1 2 3 10 12 iprod φ m Z k Z A m = seq M × k Z A
14 9 13 eqtr3id φ k Z A = seq M × k Z A
15 seqex seq M × k Z A V
16 15 a1i φ seq M × k Z A V
17 fvres m M j k Z A M j m = k Z A m
18 fzssuz M j M
19 18 1 sseqtrri M j Z
20 resmpt M j Z k Z A M j = k M j A
21 19 20 ax-mp k Z A M j = k M j A
22 21 fveq1i k Z A M j m = k M j A m
23 17 22 eqtr3di m M j k Z A m = k M j A m
24 23 prodeq2i m = M j k Z A m = m = M j k M j A m
25 prodfc m = M j k M j A m = k = M j A
26 24 25 eqtri m = M j k Z A m = k = M j A
27 eqidd φ j Z m M j k Z A m = k Z A m
28 simpr φ j Z j Z
29 28 1 eleqtrdi φ j Z j M
30 elfzuz m M j m M
31 30 1 eleqtrrdi m M j m Z
32 31 12 sylan2 φ m M j k Z A m
33 32 adantlr φ j Z m M j k Z A m
34 27 29 33 fprodser φ j Z m = M j k Z A m = seq M × k Z A j
35 26 34 eqtr3id φ j Z k = M j A = seq M × k Z A j
36 6 35 eqtr2d φ j Z seq M × k Z A j = F j
37 1 16 4 2 36 climeq φ seq M × k Z A x F x
38 37 iotabidv φ ι x | seq M × k Z A x = ι x | F x
39 df-fv seq M × k Z A = ι x | seq M × k Z A x
40 df-fv F = ι x | F x
41 38 39 40 3eqtr4g φ seq M × k Z A = F
42 14 41 eqtrd φ k Z A = F
43 8 42 breqtrrd φ F k Z A