fsum2d

Description: Write a double sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j . (Contributed by Mario Carneiro, 27-Apr-2014)

	Ref	Expression
Hypotheses	fsum2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
	fsum2d.2	$⊢ φ \to A \in Fin$
	fsum2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fsum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
Assertion	fsum2d	$⊢ φ \to \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D$

Proof

Step	Hyp	Ref	Expression
1		fsum2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
2		fsum2d.2	$⊢ φ \to A \in Fin$
3		fsum2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fsum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
5		ssid	$⊢ A \subseteq A$
6		sseq1	$⊢ w = \emptyset \to (w \subseteq A \leftrightarrow \emptyset \subseteq A)$
7		sumeq1	$⊢ w = \emptyset \to \sum_{j \in w} \sum_{k \in B} C = \sum_{j \in \emptyset} \sum_{k \in B} C$
8		iuneq1	$⊢ w = \emptyset \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in \emptyset} (\{j\} \times B)$
9	8	sumeq1d	$⊢ w = \emptyset \to \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D$
10	7 9	eqeq12d	$⊢ w = \emptyset \to (\sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \sum_{j \in \emptyset} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D)$
11	6 10	imbi12d	$⊢ w = \emptyset \to ((w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (\emptyset \subseteq A \to \sum_{j \in \emptyset} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D))$
12	11	imbi2d	$⊢ w = \emptyset \to ((φ \to (w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (\emptyset \subseteq A \to \sum_{j \in \emptyset} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D)))$
13		sseq1	$⊢ w = x \to (w \subseteq A \leftrightarrow x \subseteq A)$
14		sumeq1	$⊢ w = x \to \sum_{j \in w} \sum_{k \in B} C = \sum_{j \in x} \sum_{k \in B} C$
15		iuneq1	$⊢ w = x \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B)$
16	15	sumeq1d	$⊢ w = x \to \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
17	14 16	eqeq12d	$⊢ w = x \to (\sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D)$
18	13 17	imbi12d	$⊢ w = x \to ((w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D))$
19	18	imbi2d	$⊢ w = x \to ((φ \to (w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D)))$
20		sseq1	$⊢ w = x \cup \{y\} \to (w \subseteq A \leftrightarrow x \cup \{y\} \subseteq A)$
21		sumeq1	$⊢ w = x \cup \{y\} \to \sum_{j \in w} \sum_{k \in B} C = \sum_{j \in x \cup \{y\}} \sum_{k \in B} C$
22		iuneq1	$⊢ w = x \cup \{y\} \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in x \cup \{y\}} (\{j\} \times B)$
23	22	sumeq1d	$⊢ w = x \cup \{y\} \to \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$
24	21 23	eqeq12d	$⊢ w = x \cup \{y\} \to (\sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)$
25	20 24	imbi12d	$⊢ w = x \cup \{y\} \to ((w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
26	25	imbi2d	$⊢ w = x \cup \{y\} \to ((φ \to (w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
27		sseq1	$⊢ w = A \to (w \subseteq A \leftrightarrow A \subseteq A)$
28		sumeq1	$⊢ w = A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{j \in A} \sum_{k \in B} C$
29		iuneq1	$⊢ w = A \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
30	29	sumeq1d	$⊢ w = A \to \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D$
31	28 30	eqeq12d	$⊢ w = A \to (\sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D)$
32	27 31	imbi12d	$⊢ w = A \to ((w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (A \subseteq A \to \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D))$
33	32	imbi2d	$⊢ w = A \to ((φ \to (w \subseteq A \to \sum_{j \in w} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (A \subseteq A \to \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D)))$
34		sum0	$⊢ \sum_{z \in \emptyset} D = 0$
35		0iun	$⊢ ⋃_{j \in \emptyset} (\{j\} \times B) = \emptyset$
36	35	sumeq1i	$⊢ \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D = \sum_{z \in \emptyset} D$
37		sum0	$⊢ \sum_{j \in \emptyset} \sum_{k \in B} C = 0$
38	34 36 37	3eqtr4ri	$⊢ \sum_{j \in \emptyset} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D$
39	38	2a1i	$⊢ φ \to (\emptyset \subseteq A \to \sum_{j \in \emptyset} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in \emptyset} (\{j\} \times B)} D)$
40		ssun1	$⊢ x \subseteq x \cup \{y\}$
41		sstr	$⊢ (x \subseteq x \cup \{y\} \land x \cup \{y\} \subseteq A) \to x \subseteq A$
42	40 41	mpan	$⊢ x \cup \{y\} \subseteq A \to x \subseteq A$
43	42	imim1i	$⊢ (x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D)$
44		simpll	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to φ$
45	44 2	syl	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to A \in Fin$
46	44 3	sylan	$⊢ (((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \land j \in A) \to B \in Fin$
47	44 4	sylan	$⊢ (((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \land (j \in A \land k \in B)) \to C \in ℂ$
48		simplr	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to \neg y \in x$
49		simpr	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to x \cup \{y\} \subseteq A$
50		biid	$⊢ \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D \leftrightarrow \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
51	1 45 46 47 48 49 50	fsum2dlem	$⊢ (((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \land \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$
52	51	exp31	$⊢ (φ \land \neg y \in x) \to (x \cup \{y\} \subseteq A \to (\sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
53	52	a2d	$⊢ (φ \land \neg y \in x) \to ((x \cup \{y\} \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
54	43 53	syl5	$⊢ (φ \land \neg y \in x) \to ((x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
55	54	expcom	$⊢ \neg y \in x \to (φ \to ((x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
56	55	a2d	$⊢ \neg y \in x \to ((φ \to (x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D)) \to (φ \to (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
57	56	adantl	$⊢ (x \in Fin \land \neg y \in x) \to ((φ \to (x \subseteq A \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D)) \to (φ \to (x \cup \{y\} \subseteq A \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
58	12 19 26 33 39 57	findcard2s	$⊢ A \in Fin \to (φ \to (A \subseteq A \to \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D))$
59	2 58	mpcom	$⊢ φ \to (A \subseteq A \to \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D)$
60	5 59	mpi	$⊢ φ \to \sum_{j \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in A} (\{j\} \times B)} D$

Metamath Proof Explorer

Theorem fsum2d

Proof