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 𝑘 𝜑
sge0xp.z ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
sge0xp.a ( 𝜑𝐴𝑉 )
sge0xp.b ( 𝜑𝐵𝑊 )
sge0xp.d ( ( 𝜑𝑗𝐴𝑘𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion sge0xp ( 𝜑 → ( Σ^ ‘ ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 sge0xp.1 𝑘 𝜑
2 sge0xp.z ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
3 sge0xp.a ( 𝜑𝐴𝑉 )
4 sge0xp.b ( 𝜑𝐵𝑊 )
5 sge0xp.d ( ( 𝜑𝑗𝐴𝑘𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 snex { 𝑗 } ∈ V
7 6 a1i ( 𝜑 → { 𝑗 } ∈ V )
8 7 4 xpexd ( 𝜑 → ( { 𝑗 } × 𝐵 ) ∈ V )
9 8 adantr ( ( 𝜑𝑗𝐴 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
10 disjsnxp Disj 𝑗𝐴 ( { 𝑗 } × 𝐵 )
11 10 a1i ( 𝜑Disj 𝑗𝐴 ( { 𝑗 } × 𝐵 ) )
12 vex 𝑗 ∈ V
13 elsnxp ( 𝑗 ∈ V → ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) )
14 12 13 ax-mp ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
15 14 biimpi ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ∃ 𝑘𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
16 15 adantl ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
17 nfv 𝑘 𝑗𝐴
18 1 17 nfan 𝑘 ( 𝜑𝑗𝐴 )
19 nfv 𝑘 𝑧 ∈ ( { 𝑗 } × 𝐵 )
20 18 19 nfan 𝑘 ( ( 𝜑𝑗𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
21 nfv 𝑘 𝐷 ∈ ( 0 [,] +∞ )
22 2 3ad2ant3 ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑘𝐵𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐷 = 𝐶 )
23 5 3expa ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑘𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
24 23 3adant3 ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑘𝐵𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐶 ∈ ( 0 [,] +∞ ) )
25 22 24 eqeltrd ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑘𝐵𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐷 ∈ ( 0 [,] +∞ ) )
26 25 3exp ( ( 𝜑𝑗𝐴 ) → ( 𝑘𝐵 → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
27 26 adantr ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑘𝐵 → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
28 20 21 27 rexlimd ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( ∃ 𝑘𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 ∈ ( 0 [,] +∞ ) ) )
29 16 28 mpd ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
30 29 3impa ( ( 𝜑𝑗𝐴𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
31 3 9 11 30 sge0iunmpt ( 𝜑 → ( Σ^ ‘ ( 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) )
32 iunxpconst 𝑗𝐴 ( { 𝑗 } × 𝐵 ) = ( 𝐴 × 𝐵 )
33 32 eqcomi ( 𝐴 × 𝐵 ) = 𝑗𝐴 ( { 𝑗 } × 𝐵 )
34 33 a1i ( 𝜑 → ( 𝐴 × 𝐵 ) = 𝑗𝐴 ( { 𝑗 } × 𝐵 ) )
35 34 mpteq1d ( 𝜑 → ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) = ( 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) )
36 35 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) )
37 nfv 𝑗 𝜑
38 nfv 𝑧 ( 𝜑𝑗𝐴 )
39 4 adantr ( ( 𝜑𝑗𝐴 ) → 𝐵𝑊 )
40 simpr ( ( 𝜑𝑗𝐴 ) → 𝑗𝐴 )
41 eqid ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) = ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ )
42 40 41 projf1o ( ( 𝜑𝑗𝐴 ) → ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) : 𝐵1-1-onto→ ( { 𝑗 } × 𝐵 ) )
43 eqidd ( ( 𝜑𝑘𝐵 ) → ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) = ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) )
44 opeq2 ( 𝑖 = 𝑘 → ⟨ 𝑗 , 𝑖 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
45 44 adantl ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑖 = 𝑘 ) → ⟨ 𝑗 , 𝑖 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
46 simpr ( ( 𝜑𝑘𝐵 ) → 𝑘𝐵 )
47 opex 𝑗 , 𝑘 ⟩ ∈ V
48 47 a1i ( ( 𝜑𝑘𝐵 ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ V )
49 43 45 46 48 fvmptd ( ( 𝜑𝑘𝐵 ) → ( ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) ‘ 𝑘 ) = ⟨ 𝑗 , 𝑘 ⟩ )
50 49 adantlr ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑘𝐵 ) → ( ( 𝑖𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) ‘ 𝑘 ) = ⟨ 𝑗 , 𝑘 ⟩ )
51 38 18 2 39 42 50 29 sge0f1o ( ( 𝜑𝑗𝐴 ) → ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) )
52 51 eqcomd ( ( 𝜑𝑗𝐴 ) → ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) )
53 37 52 mpteq2da ( 𝜑 → ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) ) = ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) )
54 53 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) )
55 31 36 54 3eqtr4rd ( 𝜑 → ( Σ^ ‘ ( 𝑗𝐴 ↦ ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) )