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