gsum2d

Description: Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

	Ref	Expression
Hypotheses	gsum2d.b	$⊢ B = {Base}_{G}$
	gsum2d.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsum2d.g	$⊢ φ \to G \in CMnd$
	gsum2d.a	$⊢ φ \to A \in V$
	gsum2d.r	$⊢ φ \to Rel A$
	gsum2d.d	$⊢ φ \to D \in W$
	gsum2d.s	$⊢ φ \to dom A \subseteq D$
	gsum2d.f	$⊢ φ \to F : A ⟶ B$
	gsum2d.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
Assertion	gsum2d	$⊢ φ \to \sum_{G} F = \underset{j \in D}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$

Proof

Step	Hyp	Ref	Expression
1		gsum2d.b	$⊢ B = {Base}_{G}$
2		gsum2d.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsum2d.g	$⊢ φ \to G \in CMnd$
4		gsum2d.a	$⊢ φ \to A \in V$
5		gsum2d.r	$⊢ φ \to Rel A$
6		gsum2d.d	$⊢ φ \to D \in W$
7		gsum2d.s	$⊢ φ \to dom A \subseteq D$
8		gsum2d.f	$⊢ φ \to F : A ⟶ B$
9		gsum2d.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
10	1 2 3 4 5 6 7 8 9	gsum2dlem2	$⊢ φ \to \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
11		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
12	11 8	fssdm	$⊢ φ \to F supp \underset{˙}{0} \subseteq A$
13		relss	$⊢ F supp \underset{˙}{0} \subseteq A \to (Rel A \to Rel {supp}_{\underset{˙}{0}} (F))$
14	12 5 13	sylc	$⊢ φ \to Rel {supp}_{\underset{˙}{0}} (F)$
15		relssdmrn	$⊢ Rel {supp}_{\underset{˙}{0}} (F) \to F supp \underset{˙}{0} \subseteq dom {supp}_{\underset{˙}{0}} (F) \times ran {supp}_{\underset{˙}{0}} (F)$
16		ssv	$⊢ ran {supp}_{\underset{˙}{0}} (F) \subseteq V$
17		xpss2	$⊢ ran {supp}_{\underset{˙}{0}} (F) \subseteq V \to dom {supp}_{\underset{˙}{0}} (F) \times ran {supp}_{\underset{˙}{0}} (F) \subseteq dom {supp}_{\underset{˙}{0}} (F) \times V$
18	16 17	ax-mp	$⊢ dom {supp}_{\underset{˙}{0}} (F) \times ran {supp}_{\underset{˙}{0}} (F) \subseteq dom {supp}_{\underset{˙}{0}} (F) \times V$
19	15 18	sstrdi	$⊢ Rel {supp}_{\underset{˙}{0}} (F) \to F supp \underset{˙}{0} \subseteq dom {supp}_{\underset{˙}{0}} (F) \times V$
20	14 19	syl	$⊢ φ \to F supp \underset{˙}{0} \subseteq dom {supp}_{\underset{˙}{0}} (F) \times V$
21	12 20	ssind	$⊢ φ \to F supp \underset{˙}{0} \subseteq A \cap (dom {supp}_{\underset{˙}{0}} (F) \times V)$
22		df-res	$⊢ {A ↾}_{dom {supp}_{\underset{˙}{0}} (F)} = A \cap (dom {supp}_{\underset{˙}{0}} (F) \times V)$
23	21 22	sseqtrrdi	$⊢ φ \to F supp \underset{˙}{0} \subseteq {A ↾}_{dom {supp}_{\underset{˙}{0}} (F)}$
24	1 2 3 4 8 23 9	gsumres	$⊢ φ \to \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \sum_{G} F$
25		dmss	$⊢ F supp \underset{˙}{0} \subseteq A \to dom {supp}_{\underset{˙}{0}} (F) \subseteq dom A$
26	12 25	syl	$⊢ φ \to dom {supp}_{\underset{˙}{0}} (F) \subseteq dom A$
27	26 7	sstrd	$⊢ φ \to dom {supp}_{\underset{˙}{0}} (F) \subseteq D$
28	27	resmptd	$⊢ φ \to {(j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) ↾}_{dom {supp}_{\underset{˙}{0}} (F)} = (j \in dom {supp}_{\underset{˙}{0}} (F) ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
29	28	oveq2d	$⊢ φ \to \sum_{G} ({(j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) ↾}_{dom {supp}_{\underset{˙}{0}} (F)}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
30	1 2 3 4 5 6 7 8 9	gsum2dlem1	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B$
31	30	adantr	$⊢ (φ \land j \in D) \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B$
32	31	fmpttd	$⊢ φ \to (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) : D ⟶ B$
33		vex	$⊢ j \in V$
34		vex	$⊢ k \in V$
35	33 34	elimasn	$⊢ k \in A [\{j\}] \leftrightarrow ⟨j, k⟩ \in A$
36	35	biimpi	$⊢ k \in A [\{j\}] \to ⟨j, k⟩ \in A$
37	36	ad2antll	$⊢ (φ \land (j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F)) \land k \in A [\{j\}])) \to ⟨j, k⟩ \in A$
38		eldifn	$⊢ j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F)) \to \neg j \in dom {supp}_{\underset{˙}{0}} (F)$
39	38	ad2antrl	$⊢ (φ \land (j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F)) \land k \in A [\{j\}])) \to \neg j \in dom {supp}_{\underset{˙}{0}} (F)$
40	33 34	opeldm	$⊢ ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F) \to j \in dom {supp}_{\underset{˙}{0}} (F)$
41	39 40	nsyl	$⊢ (φ \land (j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F)) \land k \in A [\{j\}])) \to \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)$
42	37 41	eldifd	$⊢ (φ \land (j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F)) \land k \in A [\{j\}])) \to ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))$
43		df-ov	$⊢ j F k = F (⟨j, k⟩)$
44		ssidd	$⊢ φ \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
45	2	fvexi	$⊢ \underset{˙}{0} \in V$
46	45	a1i	$⊢ φ \to \underset{˙}{0} \in V$
47	8 44 4 46	suppssr	$⊢ (φ \land ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))) \to F (⟨j, k⟩) = \underset{˙}{0}$
48	43 47	syl5eq	$⊢ (φ \land ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))) \to j F k = \underset{˙}{0}$
49	42 48	syldan	$⊢ (φ \land (j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F)) \land k \in A [\{j\}])) \to j F k = \underset{˙}{0}$
50	49	anassrs	$⊢ ((φ \land j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F))) \land k \in A [\{j\}]) \to j F k = \underset{˙}{0}$
51	50	mpteq2dva	$⊢ (φ \land j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F))) \to (k \in A [\{j\}] ⟼ j F k) = (k \in A [\{j\}] ⟼ \underset{˙}{0})$
52	51	oveq2d	$⊢ (φ \land j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F))) \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \underset{k \in A [\{j\}]}{\sum_{G}} \underset{˙}{0}$
53		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
54	3 53	syl	$⊢ φ \to G \in Mnd$
55		imaexg	$⊢ A \in V \to A [\{j\}] \in V$
56	4 55	syl	$⊢ φ \to A [\{j\}] \in V$
57	2	gsumz	$⊢ (G \in Mnd \land A [\{j\}] \in V) \to \underset{k \in A [\{j\}]}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
58	54 56 57	syl2anc	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
59	58	adantr	$⊢ (φ \land j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F))) \to \underset{k \in A [\{j\}]}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
60	52 59	eqtrd	$⊢ (φ \land j \in (D ∖ dom {supp}_{\underset{˙}{0}} (F))) \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \underset{˙}{0}$
61	60 6	suppss2	$⊢ φ \to (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) supp \underset{˙}{0} \subseteq dom {supp}_{\underset{˙}{0}} (F)$
62		funmpt	$⊢ Fun (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
63	62	a1i	$⊢ φ \to Fun (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
64	9	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
65		dmfi	$⊢ F supp \underset{˙}{0} \in Fin \to dom {supp}_{\underset{˙}{0}} (F) \in Fin$
66	64 65	syl	$⊢ φ \to dom {supp}_{\underset{˙}{0}} (F) \in Fin$
67	66 61	ssfid	$⊢ φ \to (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) supp \underset{˙}{0} \in Fin$
68	6	mptexd	$⊢ φ \to (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) \in V$
69		isfsupp	$⊢ ((j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))) \leftrightarrow (Fun (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) \land (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) supp \underset{˙}{0} \in Fin))$
70	68 46 69	syl2anc	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} ((j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))) \leftrightarrow (Fun (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) \land (j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) supp \underset{˙}{0} \in Fin))$
71	63 67 70	mpbir2and	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)))$
72	1 2 3 6 32 61 71	gsumres	$⊢ φ \to \sum_{G} ({(j \in D ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) ↾}_{dom {supp}_{\underset{˙}{0}} (F)}) = \underset{j \in D}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
73	29 72	eqtr3d	$⊢ φ \to \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = \underset{j \in D}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
74	10 24 73	3eqtr3d	$⊢ φ \to \sum_{G} F = \underset{j \in D}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$

Metamath Proof Explorer

Theorem gsum2d

Proof