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 snex
 |-  { 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 ) ) )