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		vsnex	⊢ { 𝑗 } ∈ 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	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) )