Metamath Proof Explorer


Theorem sge0xp

Description: Combine two generalized sums of nonnegative extended reals into a single generalized sum over the cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0xp.1 k φ
sge0xp.z z = j k D = C
sge0xp.a φ A V
sge0xp.b φ B W
sge0xp.d φ j A k B C 0 +∞
Assertion sge0xp φ sum^ j A sum^ k B C = sum^ z A × B D

Proof

Step Hyp Ref Expression
1 sge0xp.1 k φ
2 sge0xp.z z = j k D = C
3 sge0xp.a φ A V
4 sge0xp.b φ B W
5 sge0xp.d φ j A k B C 0 +∞
6 snex j V
7 6 a1i φ j V
8 7 4 xpexd φ j × B V
9 8 adantr φ j A j × B V
10 disjsnxp Disj j A j × B
11 10 a1i φ Disj j A j × B
12 vex j V
13 elsnxp j V z j × B k B z = j k
14 12 13 ax-mp z j × B k B z = j k
15 14 biimpi z j × B k B z = j k
16 15 adantl φ j A z j × B k B z = j k
17 nfv k j A
18 1 17 nfan k φ j A
19 nfv k z j × B
20 18 19 nfan k φ j A z j × B
21 nfv k D 0 +∞
22 2 3ad2ant3 φ j A k B z = j k D = C
23 5 3expa φ j A k B C 0 +∞
24 23 3adant3 φ j A k B z = j k C 0 +∞
25 22 24 eqeltrd φ j A k B z = j k D 0 +∞
26 25 3exp φ j A k B z = j k D 0 +∞
27 26 adantr φ j A z j × B k B z = j k D 0 +∞
28 20 21 27 rexlimd φ j A z j × B k B z = j k D 0 +∞
29 16 28 mpd φ j A z j × B D 0 +∞
30 29 3impa φ j A z j × B D 0 +∞
31 3 9 11 30 sge0iunmpt φ sum^ z j A j × B D = sum^ j A sum^ z j × B D
32 iunxpconst j A j × B = A × B
33 32 eqcomi A × B = j A j × B
34 33 a1i φ A × B = j A j × B
35 34 mpteq1d φ z A × B D = z j A j × B D
36 35 fveq2d φ sum^ z A × B D = sum^ z j A j × B D
37 nfv j φ
38 nfv z φ j A
39 4 adantr φ j A B W
40 simpr φ j A j A
41 eqid i B j i = i B j i
42 40 41 projf1o φ j A i B j i : B 1-1 onto j × B
43 eqidd φ k B i B j i = i B j i
44 opeq2 i = k j i = j k
45 44 adantl φ k B i = k j i = j k
46 simpr φ k B k B
47 opex j k V
48 47 a1i φ k B j k V
49 43 45 46 48 fvmptd φ k B i B j i k = j k
50 49 adantlr φ j A k B i B j i k = j k
51 38 18 2 39 42 50 29 sge0f1o φ j A sum^ z j × B D = sum^ k B C
52 51 eqcomd φ j A sum^ k B C = sum^ z j × B D
53 37 52 mpteq2da φ j A sum^ k B C = j A sum^ z j × B D
54 53 fveq2d φ sum^ j A sum^ k B C = sum^ j A sum^ z j × B D
55 31 36 54 3eqtr4rd φ sum^ j A sum^ k B C = sum^ z A × B D