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	$⊢ Ⅎ k φ$
	sge0xp.z	$⊢ z = ⟨j, k⟩ \to D = C$
	sge0xp.a	$⊢ φ \to A \in V$
	sge0xp.b	$⊢ φ \to B \in W$
	sge0xp.d	$⊢ (φ \land j \in A \land k \in B) \to C \in [0, +∞]$
Assertion	sge0xp	$⊢ φ \to sum^((j \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((z \in (A \times B) ⟼ D))$

Proof

Step	Hyp	Ref	Expression
1		sge0xp.1	$⊢ Ⅎ k φ$
2		sge0xp.z	$⊢ z = ⟨j, k⟩ \to D = C$
3		sge0xp.a	$⊢ φ \to A \in V$
4		sge0xp.b	$⊢ φ \to B \in W$
5		sge0xp.d	$⊢ (φ \land j \in A \land k \in B) \to C \in [0, +∞]$
6		vsnex	$⊢ \{j\} \in V$
7	6	a1i	$⊢ φ \to \{j\} \in V$
8	7 4	xpexd	$⊢ φ \to \{j\} \times B \in V$
9	8	adantr	$⊢ (φ \land j \in A) \to \{j\} \times B \in V$
10		disjsnxp	$⊢ \underset{j \in A}{Disj} (\{j\} \times B)$
11	10	a1i	$⊢ φ \to \underset{j \in A}{Disj} (\{j\} \times B)$
12		vex	$⊢ j \in V$
13		elsnxp	$⊢ j \in V \to (z \in (\{j\} \times B) \leftrightarrow \exists k \in B z = ⟨j, k⟩)$
14	12 13	ax-mp	$⊢ z \in (\{j\} \times B) \leftrightarrow \exists k \in B z = ⟨j, k⟩$
15	14	bilani	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to \exists k \in B z = ⟨j, k⟩$
16		nfv	$⊢ Ⅎ k j \in A$
17	1 16	nfan	$⊢ Ⅎ k (φ \land j \in A)$
18		nfv	$⊢ Ⅎ k z \in (\{j\} \times B)$
19	17 18	nfan	$⊢ Ⅎ k ((φ \land j \in A) \land z \in (\{j\} \times B))$
20		nfv	$⊢ Ⅎ k D \in [0, +∞]$
21	2	3ad2ant3	$⊢ ((φ \land j \in A) \land k \in B \land z = ⟨j, k⟩) \to D = C$
22	5	3expa	$⊢ ((φ \land j \in A) \land k \in B) \to C \in [0, +∞]$
23	22	3adant3	$⊢ ((φ \land j \in A) \land k \in B \land z = ⟨j, k⟩) \to C \in [0, +∞]$
24	21 23	eqeltrd	$⊢ ((φ \land j \in A) \land k \in B \land z = ⟨j, k⟩) \to D \in [0, +∞]$
25	24	3exp	$⊢ (φ \land j \in A) \to (k \in B \to (z = ⟨j, k⟩ \to D \in [0, +∞]))$
26	25	adantr	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to (k \in B \to (z = ⟨j, k⟩ \to D \in [0, +∞]))$
27	19 20 26	rexlimd	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to (\exists k \in B z = ⟨j, k⟩ \to D \in [0, +∞])$
28	15 27	mpd	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to D \in [0, +∞]$
29	28	3impa	$⊢ (φ \land j \in A \land z \in (\{j\} \times B)) \to D \in [0, +∞]$
30	3 9 11 29	sge0iunmpt	$⊢ φ \to sum^((z \in ⋃_{j \in A} (\{j\} \times B) ⟼ D)) = sum^((j \in A ⟼ sum^((z \in (\{j\} \times B) ⟼ D))))$
31		iunxpconst	$⊢ ⋃_{j \in A} (\{j\} \times B) = A \times B$
32	31	eqcomi	$⊢ A \times B = ⋃_{j \in A} (\{j\} \times B)$
33	32	a1i	$⊢ φ \to A \times B = ⋃_{j \in A} (\{j\} \times B)$
34	33	mpteq1d	$⊢ φ \to (z \in (A \times B) ⟼ D) = (z \in ⋃_{j \in A} (\{j\} \times B) ⟼ D)$
35	34	fveq2d	$⊢ φ \to sum^((z \in (A \times B) ⟼ D)) = sum^((z \in ⋃_{j \in A} (\{j\} \times B) ⟼ D))$
36		nfv	$⊢ Ⅎ j φ$
37		nfv	$⊢ Ⅎ z (φ \land j \in A)$
38	4	adantr	$⊢ (φ \land j \in A) \to B \in W$
39		simpr	$⊢ (φ \land j \in A) \to j \in A$
40		eqid	$⊢ (i \in B ⟼ ⟨j, i⟩) = (i \in B ⟼ ⟨j, i⟩)$
41	39 40	projf1o	$⊢ (φ \land j \in A) \to (i \in B ⟼ ⟨j, i⟩) : B \underset{1-1 onto}{⟶} \{j\} \times B$
42		eqidd	$⊢ (φ \land k \in B) \to (i \in B ⟼ ⟨j, i⟩) = (i \in B ⟼ ⟨j, i⟩)$
43		opeq2	$⊢ i = k \to ⟨j, i⟩ = ⟨j, k⟩$
44	43	adantl	$⊢ ((φ \land k \in B) \land i = k) \to ⟨j, i⟩ = ⟨j, k⟩$
45		simpr	$⊢ (φ \land k \in B) \to k \in B$
46		opex	$⊢ ⟨j, k⟩ \in V$
47	46	a1i	$⊢ (φ \land k \in B) \to ⟨j, k⟩ \in V$
48	42 44 45 47	fvmptd	$⊢ (φ \land k \in B) \to (i \in B ⟼ ⟨j, i⟩) (k) = ⟨j, k⟩$
49	48	adantlr	$⊢ ((φ \land j \in A) \land k \in B) \to (i \in B ⟼ ⟨j, i⟩) (k) = ⟨j, k⟩$
50	37 17 2 38 41 49 28	sge0f1o	$⊢ (φ \land j \in A) \to sum^((z \in (\{j\} \times B) ⟼ D)) = sum^((k \in B ⟼ C))$
51	50	eqcomd	$⊢ (φ \land j \in A) \to sum^((k \in B ⟼ C)) = sum^((z \in (\{j\} \times B) ⟼ D))$
52	36 51	mpteq2da	$⊢ φ \to (j \in A ⟼ sum^((k \in B ⟼ C))) = (j \in A ⟼ sum^((z \in (\{j\} \times B) ⟼ D)))$
53	52	fveq2d	$⊢ φ \to sum^((j \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((j \in A ⟼ sum^((z \in (\{j\} \times B) ⟼ D))))$
54	30 35 53	3eqtr4rd	$⊢ φ \to sum^((j \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((z \in (A \times B) ⟼ D))$

Metamath Proof Explorer

Theorem sge0xp

Proof