gsum2d2

Description: Write a group sum over a two-dimensional region as a double sum. Note that C ( j ) is a function of j . (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	gsum2d2.b	$⊢ B = {Base}_{G}$
	gsum2d2.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsum2d2.g	$⊢ φ \to G \in CMnd$
	gsum2d2.a	$⊢ φ \to A \in V$
	gsum2d2.r	$⊢ (φ \land j \in A) \to C \in W$
	gsum2d2.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
	gsum2d2.u	$⊢ φ \to U \in Fin$
	gsum2d2.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
Assertion	gsum2d2	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, X)$

Proof

Step	Hyp	Ref	Expression
1		gsum2d2.b	$⊢ B = {Base}_{G}$
2		gsum2d2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsum2d2.g	$⊢ φ \to G \in CMnd$
4		gsum2d2.a	$⊢ φ \to A \in V$
5		gsum2d2.r	$⊢ (φ \land j \in A) \to C \in W$
6		gsum2d2.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
7		gsum2d2.u	$⊢ φ \to U \in Fin$
8		gsum2d2.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
9		snex	$⊢ \{j\} \in V$
10		xpexg	$⊢ (\{j\} \in V \land C \in W) \to \{j\} \times C \in V$
11	9 5 10	sylancr	$⊢ (φ \land j \in A) \to \{j\} \times C \in V$
12	11	ralrimiva	$⊢ φ \to \forall j \in A \{j\} \times C \in V$
13		iunexg	$⊢ (A \in V \land \forall j \in A \{j\} \times C \in V) \to ⋃_{j \in A} (\{j\} \times C) \in V$
14	4 12 13	syl2anc	$⊢ φ \to ⋃_{j \in A} (\{j\} \times C) \in V$
15		relxp	$⊢ Rel (\{j\} \times C)$
16	15	rgenw	$⊢ \forall j \in A Rel (\{j\} \times C)$
17		reliun	$⊢ Rel ⋃_{j \in A} (\{j\} \times C) \leftrightarrow \forall j \in A Rel (\{j\} \times C)$
18	16 17	mpbir	$⊢ Rel ⋃_{j \in A} (\{j\} \times C)$
19	18	a1i	$⊢ φ \to Rel ⋃_{j \in A} (\{j\} \times C)$
20		vex	$⊢ x \in V$
21	20	eldm2	$⊢ x \in dom ⋃_{j \in A} (\{j\} \times C) \leftrightarrow \exists y ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C)$
22		eliunxp	$⊢ ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow \exists j \exists k (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in C))$
23		vex	$⊢ y \in V$
24	20 23	opth1	$⊢ ⟨x, y⟩ = ⟨j, k⟩ \to x = j$
25	24	ad2antrl	$⊢ (φ \land (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in C))) \to x = j$
26		simprrl	$⊢ (φ \land (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in C))) \to j \in A$
27	25 26	eqeltrd	$⊢ (φ \land (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in C))) \to x \in A$
28	27	ex	$⊢ φ \to ((⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in C)) \to x \in A)$
29	28	exlimdvv	$⊢ φ \to (\exists j \exists k (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in C)) \to x \in A)$
30	22 29	syl5bi	$⊢ φ \to (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \to x \in A)$
31	30	exlimdv	$⊢ φ \to (\exists y ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times C) \to x \in A)$
32	21 31	syl5bi	$⊢ φ \to (x \in dom ⋃_{j \in A} (\{j\} \times C) \to x \in A)$
33	32	ssrdv	$⊢ φ \to dom ⋃_{j \in A} (\{j\} \times C) \subseteq A$
34	6	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in C X \in B$
35		eqid	$⊢ (j \in A, k \in C ⟼ X) = (j \in A, k \in C ⟼ X)$
36	35	fmpox	$⊢ \forall j \in A \forall k \in C X \in B \leftrightarrow (j \in A, k \in C ⟼ X) : ⋃_{j \in A} (\{j\} \times C) ⟶ B$
37	34 36	sylib	$⊢ φ \to (j \in A, k \in C ⟼ X) : ⋃_{j \in A} (\{j\} \times C) ⟶ B$
38	1 2 3 4 5 6 7 8	gsum2d2lem	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((j \in A, k \in C ⟼ X))$
39	1 2 3 14 19 4 33 37 38	gsum2d	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \underset{m \in A}{\sum_{G}} (\underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}]}{\sum_{G}}, (m (j \in A, k \in C ⟼ X) n))$
40		nfcv	$⊢ \underline{Ⅎ} j G$
41		nfcv	$⊢ \underline{Ⅎ} j Σ_{𝑔}$
42		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times C)$
43		nfcv	$⊢ \underline{Ⅎ} j \{m\}$
44	42 43	nfima	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times C) [\{m\}]$
45		nfcv	$⊢ \underline{Ⅎ} j m$
46		nfmpo1	$⊢ \underline{Ⅎ} j (j \in A, k \in C ⟼ X)$
47		nfcv	$⊢ \underline{Ⅎ} j n$
48	45 46 47	nfov	$⊢ \underline{Ⅎ} j (m (j \in A, k \in C ⟼ X) n)$
49	44 48	nfmpt	$⊢ \underline{Ⅎ} j (n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}] ⟼ m (j \in A, k \in C ⟼ X) n)$
50	40 41 49	nfov	$⊢ \underline{Ⅎ} j (\underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}]}{\sum_{G}}, (m (j \in A, k \in C ⟼ X) n))$
51		nfcv	$⊢ \underline{Ⅎ} m (\underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}]}{\sum_{G}}, (j (j \in A, k \in C ⟼ X) n))$
52		sneq	$⊢ m = j \to \{m\} = \{j\}$
53	52	imaeq2d	$⊢ m = j \to ⋃_{j \in A} (\{j\} \times C) [\{m\}] = ⋃_{j \in A} (\{j\} \times C) [\{j\}]$
54		oveq1	$⊢ m = j \to m (j \in A, k \in C ⟼ X) n = j (j \in A, k \in C ⟼ X) n$
55	53 54	mpteq12dv	$⊢ m = j \to (n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}] ⟼ m (j \in A, k \in C ⟼ X) n) = (n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] ⟼ j (j \in A, k \in C ⟼ X) n)$
56	55	oveq2d	$⊢ m = j \to \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}]}{\sum_{G}} (m (j \in A, k \in C ⟼ X) n) = \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}]}{\sum_{G}} (j (j \in A, k \in C ⟼ X) n)$
57	50 51 56	cbvmpt	$⊢ (m \in A ⟼ \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}]}{\sum_{G}} (m (j \in A, k \in C ⟼ X) n)) = (j \in A ⟼ \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}]}{\sum_{G}} (j (j \in A, k \in C ⟼ X) n))$
58		vex	$⊢ j \in V$
59		vex	$⊢ k \in V$
60	58 59	elimasn	$⊢ k \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] \leftrightarrow ⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C)$
61		opeliunxp	$⊢ ⟨j, k⟩ \in ⋃_{j \in A} (\{j\} \times C) \leftrightarrow (j \in A \land k \in C)$
62	60 61	bitri	$⊢ k \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] \leftrightarrow (j \in A \land k \in C)$
63	62	baib	$⊢ j \in A \to (k \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] \leftrightarrow k \in C)$
64	63	eqrdv	$⊢ j \in A \to ⋃_{j \in A} (\{j\} \times C) [\{j\}] = C$
65	64	mpteq1d	$⊢ j \in A \to (n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] ⟼ j (j \in A, k \in C ⟼ X) n) = (n \in C ⟼ j (j \in A, k \in C ⟼ X) n)$
66		nfcv	$⊢ \underline{Ⅎ} k j$
67		nfmpo2	$⊢ \underline{Ⅎ} k (j \in A, k \in C ⟼ X)$
68		nfcv	$⊢ \underline{Ⅎ} k n$
69	66 67 68	nfov	$⊢ \underline{Ⅎ} k (j (j \in A, k \in C ⟼ X) n)$
70		nfcv	$⊢ \underline{Ⅎ} n (j (j \in A, k \in C ⟼ X) k)$
71		oveq2	$⊢ n = k \to j (j \in A, k \in C ⟼ X) n = j (j \in A, k \in C ⟼ X) k$
72	69 70 71	cbvmpt	$⊢ (n \in C ⟼ j (j \in A, k \in C ⟼ X) n) = (k \in C ⟼ j (j \in A, k \in C ⟼ X) k)$
73	65 72	eqtrdi	$⊢ j \in A \to (n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] ⟼ j (j \in A, k \in C ⟼ X) n) = (k \in C ⟼ j (j \in A, k \in C ⟼ X) k)$
74	73	adantl	$⊢ (φ \land j \in A) \to (n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] ⟼ j (j \in A, k \in C ⟼ X) n) = (k \in C ⟼ j (j \in A, k \in C ⟼ X) k)$
75		simprl	$⊢ (φ \land (j \in A \land k \in C)) \to j \in A$
76		simprr	$⊢ (φ \land (j \in A \land k \in C)) \to k \in C$
77	35	ovmpt4g	$⊢ (j \in A \land k \in C \land X \in B) \to j (j \in A, k \in C ⟼ X) k = X$
78	75 76 6 77	syl3anc	$⊢ (φ \land (j \in A \land k \in C)) \to j (j \in A, k \in C ⟼ X) k = X$
79	78	anassrs	$⊢ ((φ \land j \in A) \land k \in C) \to j (j \in A, k \in C ⟼ X) k = X$
80	79	mpteq2dva	$⊢ (φ \land j \in A) \to (k \in C ⟼ j (j \in A, k \in C ⟼ X) k) = (k \in C ⟼ X)$
81	74 80	eqtrd	$⊢ (φ \land j \in A) \to (n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}] ⟼ j (j \in A, k \in C ⟼ X) n) = (k \in C ⟼ X)$
82	81	oveq2d	$⊢ (φ \land j \in A) \to \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}]}{\sum_{G}} (j (j \in A, k \in C ⟼ X) n) = \underset{k \in C}{\sum_{G}} X$
83	82	mpteq2dva	$⊢ φ \to (j \in A ⟼ \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{j\}]}{\sum_{G}} (j (j \in A, k \in C ⟼ X) n)) = (j \in A ⟼ \underset{k \in C}{\sum_{G}} X)$
84	57 83	syl5eq	$⊢ φ \to (m \in A ⟼ \underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}]}{\sum_{G}} (m (j \in A, k \in C ⟼ X) n)) = (j \in A ⟼ \underset{k \in C}{\sum_{G}} X)$
85	84	oveq2d	$⊢ φ \to \underset{m \in A}{\sum_{G}} (\underset{n \in ⋃_{j \in A} (\{j\} \times C) [\{m\}]}{\sum_{G}}, (m (j \in A, k \in C ⟼ X) n)) = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, X)$
86	39 85	eqtrd	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, X)$

Metamath Proof Explorer

Theorem gsum2d2

Proof