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		snex	$⊢ \{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	biimpi	$⊢ z \in (\{j\} \times B) \to \exists k \in B z = ⟨j, k⟩$
16	15	adantl	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to \exists k \in B z = ⟨j, k⟩$
17		nfv	$⊢ Ⅎ k j \in A$
18	1 17	nfan	$⊢ Ⅎ k (φ \land j \in A)$
19		nfv	$⊢ Ⅎ k z \in (\{j\} \times B)$
20	18 19	nfan	$⊢ Ⅎ k ((φ \land j \in A) \land z \in (\{j\} \times B))$
21		nfv	$⊢ Ⅎ k D \in [0, +∞]$
22	2	3ad2ant3	$⊢ ((φ \land j \in A) \land k \in B \land z = ⟨j, k⟩) \to D = C$
23	5	3expa	$⊢ ((φ \land j \in A) \land k \in B) \to C \in [0, +∞]$
24	23	3adant3	$⊢ ((φ \land j \in A) \land k \in B \land z = ⟨j, k⟩) \to C \in [0, +∞]$
25	22 24	eqeltrd	$⊢ ((φ \land j \in A) \land k \in B \land z = ⟨j, k⟩) \to D \in [0, +∞]$
26	25	3exp	$⊢ (φ \land j \in A) \to (k \in B \to (z = ⟨j, k⟩ \to D \in [0, +∞]))$
27	26	adantr	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to (k \in B \to (z = ⟨j, k⟩ \to D \in [0, +∞]))$
28	20 21 27	rexlimd	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to (\exists k \in B z = ⟨j, k⟩ \to D \in [0, +∞])$
29	16 28	mpd	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to D \in [0, +∞]$
30	29	3impa	$⊢ (φ \land j \in A \land z \in (\{j\} \times B)) \to D \in [0, +∞]$
31	3 9 11 30	sge0iunmpt	$⊢ φ \to sum^((z \in ⋃_{j \in A} (\{j\} \times B) ⟼ D)) = sum^((j \in A ⟼ sum^((z \in (\{j\} \times B) ⟼ D))))$
32		iunxpconst	$⊢ ⋃_{j \in A} (\{j\} \times B) = A \times B$
33	32	eqcomi	$⊢ A \times B = ⋃_{j \in A} (\{j\} \times B)$
34	33	a1i	$⊢ φ \to A \times B = ⋃_{j \in A} (\{j\} \times B)$
35	34	mpteq1d	$⊢ φ \to (z \in (A \times B) ⟼ D) = (z \in ⋃_{j \in A} (\{j\} \times B) ⟼ D)$
36	35	fveq2d	$⊢ φ \to sum^((z \in (A \times B) ⟼ D)) = sum^((z \in ⋃_{j \in A} (\{j\} \times B) ⟼ D))$
37		nfv	$⊢ Ⅎ j φ$
38		nfv	$⊢ Ⅎ z (φ \land j \in A)$
39	4	adantr	$⊢ (φ \land j \in A) \to B \in W$
40		simpr	$⊢ (φ \land j \in A) \to j \in A$
41		eqid	$⊢ (i \in B ⟼ ⟨j, i⟩) = (i \in B ⟼ ⟨j, i⟩)$
42	40 41	projf1o	$⊢ (φ \land j \in A) \to (i \in B ⟼ ⟨j, i⟩) : B \underset{1-1 onto}{⟶} \{j\} \times B$
43		eqidd	$⊢ (φ \land k \in B) \to (i \in B ⟼ ⟨j, i⟩) = (i \in B ⟼ ⟨j, i⟩)$
44		opeq2	$⊢ i = k \to ⟨j, i⟩ = ⟨j, k⟩$
45	44	adantl	$⊢ ((φ \land k \in B) \land i = k) \to ⟨j, i⟩ = ⟨j, k⟩$
46		simpr	$⊢ (φ \land k \in B) \to k \in B$
47		opex	$⊢ ⟨j, k⟩ \in V$
48	47	a1i	$⊢ (φ \land k \in B) \to ⟨j, k⟩ \in V$
49	43 45 46 48	fvmptd	$⊢ (φ \land k \in B) \to (i \in B ⟼ ⟨j, i⟩) (k) = ⟨j, k⟩$
50	49	adantlr	$⊢ ((φ \land j \in A) \land k \in B) \to (i \in B ⟼ ⟨j, i⟩) (k) = ⟨j, k⟩$
51	38 18 2 39 42 50 29	sge0f1o	$⊢ (φ \land j \in A) \to sum^((z \in (\{j\} \times B) ⟼ D)) = sum^((k \in B ⟼ C))$
52	51	eqcomd	$⊢ (φ \land j \in A) \to sum^((k \in B ⟼ C)) = sum^((z \in (\{j\} \times B) ⟼ D))$
53	37 52	mpteq2da	$⊢ φ \to (j \in A ⟼ sum^((k \in B ⟼ C))) = (j \in A ⟼ sum^((z \in (\{j\} \times B) ⟼ D)))$
54	53	fveq2d	$⊢ φ \to sum^((j \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((j \in A ⟼ sum^((z \in (\{j\} \times B) ⟼ D))))$
55	31 36 54	3eqtr4rd	$⊢ φ \to sum^((j \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((z \in (A \times B) ⟼ D))$

Metamath Proof Explorer

Theorem sge0xp

Proof