Metamath Proof Explorer


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 ffvelcdmda โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ( seq ๐‘€ ( ยท , ๐น ) โ€˜ ๐‘— ) โˆˆ โ„‚ )
46 1 2 10 prodf โŠข ( ๐œ‘ โ†’ seq ๐‘€ ( ยท , ๐บ ) : ๐‘ โŸถ โ„‚ )
47 46 ffvelcdmda โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ( 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 โŠข ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ๐‘ ( ๐ด ยท ๐ต ) = ( โˆ ๐‘˜ โˆˆ ๐‘ ๐ด ยท โˆ ๐‘˜ โˆˆ ๐‘ ๐ต ) )