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	bilani	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
16		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
17	1 16	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
18		nfv	⊢ Ⅎ 𝑘 𝑧 ∈ ( { 𝑗 } × 𝐵 )
19	17 18	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
20		nfv	⊢ Ⅎ 𝑘 𝐷 ∈ ( 0 [,] +∞ )
21	2	3ad2ant3	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐷 = 𝐶 )
22	5	3expa	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
23	22	3adant3	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐶 ∈ ( 0 [,] +∞ ) )
24	21 23	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐷 ∈ ( 0 [,] +∞ ) )
25	24	3exp	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑘 ∈ 𝐵 → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
27	19 20 26	rexlimd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 ∈ ( 0 [,] +∞ ) ) )
28	15 27	mpd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
29	28	3impa	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
30	3 9 11 29	sge0iunmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) )
31		iunxpconst	⊢ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ( 𝐴 × 𝐵 )
32	31	eqcomi	⊢ ( 𝐴 × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
33	32	a1i	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
34	33	mpteq1d	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) = ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) )
35	34	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) )
36		nfv	⊢ Ⅎ 𝑗 𝜑
37		nfv	⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
38	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
39		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
40		eqid	⊢ ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) = ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ )
41	39 40	projf1o	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) : 𝐵 –1-1-onto→ ( { 𝑗 } × 𝐵 ) )
42		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) = ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) )
43		opeq2	⊢ ( 𝑖 = 𝑘 → ⟨ 𝑗 , 𝑖 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
44	43	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑖 = 𝑘 ) → ⟨ 𝑗 , 𝑖 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
45		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
46		opex	⊢ ⟨ 𝑗 , 𝑘 ⟩ ∈ V
47	46	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ V )
48	42 44 45 47	fvmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) ‘ 𝑘 ) = ⟨ 𝑗 , 𝑘 ⟩ )
49	48	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑖 ⟩ ) ‘ 𝑘 ) = ⟨ 𝑗 , 𝑘 ⟩ )
50	37 17 2 38 41 49 28	sge0f1o	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
51	50	eqcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) )
52	36 51	mpteq2da	⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) )
53	52	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) )
54	30 35 53	3eqtr4rd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) )