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 
|- F/ k ph
sge0xp.z 
|- ( z = <. j , k >. -> D = C )
sge0xp.a 
|- ( ph -> A e. V )
sge0xp.b 
|- ( ph -> B e. W )
sge0xp.d 
|- ( ( ph /\ j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
Assertion sge0xp 
|- ( ph -> ( sum^ ` ( j e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( z e. ( A X. B ) |-> D ) ) )

Proof

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