Metamath Proof Explorer

Theorem iprodmul

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

Ref Expression
Hypotheses iprodmul.1 
|- Z = ( ZZ>= ` M )
iprodmul.2 
|- ( ph -> M e. ZZ )
iprodmul.3 
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
iprodmul.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
iprodmul.5 
|- ( ( ph /\ k e. Z ) -> A e. CC )
iprodmul.6 
|- ( ph -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )
iprodmul.7 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = B )
iprodmul.8 
|- ( ( ph /\ k e. Z ) -> B e. CC )
Assertion iprodmul 
|- ( ph -> prod_ k e. Z ( A x. B ) = ( prod_ k e. Z A x. prod_ k e. Z B ) )

Proof

Step Hyp Ref Expression
1 iprodmul.1 
 |-  Z = ( ZZ>= ` M )
2 iprodmul.2 
 |-  ( ph -> M e. ZZ )
3 iprodmul.3 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
4 iprodmul.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5 iprodmul.5 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
6 iprodmul.6 
 |-  ( ph -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )
7 iprodmul.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = B )
8 iprodmul.8 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
9 4 5 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
10 7 8 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
11 fveq2 
 |-  ( a = k -> ( F ` a ) = ( F ` k ) )
12 fveq2 
 |-  ( a = k -> ( G ` a ) = ( G ` k ) )
13 11 12 oveq12d 
 |-  ( a = k -> ( ( F ` a ) x. ( G ` a ) ) = ( ( F ` k ) x. ( G ` k ) ) )
14 eqid 
 |-  ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) = ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) )
15 ovex 
 |-  ( ( F ` k ) x. ( G ` k ) ) e. _V
16 13 14 15 fvmpt 
 |-  ( k e. Z -> ( ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
17 16 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
18 1 3 9 6 10 17 ntrivcvgmul 
 |-  ( ph -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( 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 ) x. ( G ` m ) ) = ( ( F ` a ) x. ( G ` a ) ) )
22 21 cbvmptv 
 |-  ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) = ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) )
23 seqeq3 
 |-  ( ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) = ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) -> seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) = seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ) )
24 22 23 ax-mp 
 |-  seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) = seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) )
25 24 breq1i 
 |-  ( seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ~~> w <-> seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ) ~~> w )
26 25 anbi2i 
 |-  ( ( w =/= 0 /\ seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ~~> w ) <-> ( w =/= 0 /\ seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ) ~~> w ) )
27 26 exbii 
 |-  ( E. w ( w =/= 0 /\ seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ~~> w ) <-> E. w ( w =/= 0 /\ seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ) ~~> w ) )
28 27 rexbii 
 |-  ( E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ~~> w ) <-> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , ( a e. Z |-> ( ( F ` a ) x. ( G ` a ) ) ) ) ~~> w ) )
29 18 28 sylibr 
 |-  ( ph -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ~~> w ) )
30 eqid 
 |-  ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) = ( m e. Z |-> ( ( F ` m ) x. ( 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 ) x. ( G ` m ) ) = ( ( F ` k ) x. ( G ` k ) ) )
34 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
35 9 10 mulcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) x. ( G ` k ) ) e. CC )
36 30 33 34 35 fvmptd3 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
37 4 7 oveq12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) x. ( G ` k ) ) = ( A x. B ) )
38 36 37 eqtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ` k ) = ( A x. B ) )
39 5 8 mulcld 
 |-  ( ( ph /\ k e. Z ) -> ( A x. B ) e. CC )
40 1 2 3 4 5 iprodclim2 
 |-  ( ph -> seq M ( x. , F ) ~~> prod_ k e. Z A )
41 seqex 
 |-  seq M ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) e. _V
42 41 a1i 
 |-  ( ph -> seq M ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) e. _V )
43 1 2 6 7 8 iprodclim2 
 |-  ( ph -> seq M ( x. , G ) ~~> prod_ k e. Z B )
44 1 2 9 prodf 
 |-  ( ph -> seq M ( x. , F ) : Z --> CC )
45 44 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( x. , F ) ` j ) e. CC )
46 1 2 10 prodf 
 |-  ( ph -> seq M ( x. , G ) : Z --> CC )
47 46 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( x. , G ) ` j ) e. CC )
48 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
49 48 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
50 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
51 50 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
52 51 9 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
53 52 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
54 51 10 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( G ` k ) e. CC )
55 54 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( G ` k ) e. CC )
56 36 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
57 51 56 sylan2 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
58 49 53 55 57 prodfmul 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ` j ) = ( ( seq M ( x. , F ) ` j ) x. ( seq M ( x. , G ) ` j ) ) )
59 1 2 40 42 43 45 47 58 climmul 
 |-  ( ph -> seq M ( x. , ( m e. Z |-> ( ( F ` m ) x. ( G ` m ) ) ) ) ~~> ( prod_ k e. Z A x. prod_ k e. Z B ) )
60 1 2 29 38 39 59 iprodclim 
 |-  ( ph -> prod_ k e. Z ( A x. B ) = ( prod_ k e. Z A x. prod_ k e. Z B ) )