gsumfs2d

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsumfs2d.p	$⊢ Ⅎ x φ$
	gsumfs2d.b	$⊢ B = {Base}_{W}$
	gsumfs2d.1	$⊢ \underset{˙}{0} = 0_{W}$
	gsumfs2d.r	$⊢ φ \to Rel A$
	gsumfs2d.2	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumfs2d.w	$⊢ φ \to W \in CMnd$
	gsumfs2d.3	$⊢ φ \to F : A ⟶ B$
	gsumfs2d.a	$⊢ φ \to A \in X$
Assertion	gsumfs2d	$⊢ φ \to \sum_{W} F = \underset{x \in dom A}{\sum_{W}} (\underset{y \in A [\{x\}]}{\sum_{W}}, F (⟨x, y⟩))$

Proof

Step	Hyp	Ref	Expression
1		gsumfs2d.p	$⊢ Ⅎ x φ$
2		gsumfs2d.b	$⊢ B = {Base}_{W}$
3		gsumfs2d.1	$⊢ \underset{˙}{0} = 0_{W}$
4		gsumfs2d.r	$⊢ φ \to Rel A$
5		gsumfs2d.2	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
6		gsumfs2d.w	$⊢ φ \to W \in CMnd$
7		gsumfs2d.3	$⊢ φ \to F : A ⟶ B$
8		gsumfs2d.a	$⊢ φ \to A \in X$
9	6	adantr	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to W \in CMnd$
10	8	adantr	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to A \in X$
11	10	imaexd	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to A [\{x\}] \in V$
12	7	ffnd	$⊢ φ \to F Fn A$
13	12	ad2antrr	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to F Fn A$
14	8	ad2antrr	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to A \in X$
15	3	fvexi	$⊢ \underset{˙}{0} \in V$
16	15	a1i	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to \underset{˙}{0} \in V$
17		simpr	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])$
18	17	eldifad	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to y \in A [\{x\}]$
19		vex	$⊢ x \in V$
20		vex	$⊢ y \in V$
21	19 20	elimasn	$⊢ y \in A [\{x\}] \leftrightarrow ⟨x, y⟩ \in A$
22	21	biimpi	$⊢ y \in A [\{x\}] \to ⟨x, y⟩ \in A$
23	18 22	syl	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to ⟨x, y⟩ \in A$
24	17	eldifbd	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]$
25	19 20	elimasn	$⊢ y \in {supp}_{\underset{˙}{0}} (F) [\{x\}] \leftrightarrow ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F)$
26	25	biimpri	$⊢ ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F) \to y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]$
27	24 26	nsyl	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to \neg ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F)$
28	23 27	eldifd	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to ⟨x, y⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))$
29	13 14 16 28	fvdifsupp	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in (A [\{x\}] ∖ {supp}_{\underset{˙}{0}} (F) [\{x\}])) \to F (⟨x, y⟩) = \underset{˙}{0}$
30	5	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
31	30	adantr	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to F supp \underset{˙}{0} \in Fin$
32		imafi2	$⊢ F supp \underset{˙}{0} \in Fin \to {supp}_{\underset{˙}{0}} (F) [\{x\}] \in Fin$
33	31 32	syl	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to {supp}_{\underset{˙}{0}} (F) [\{x\}] \in Fin$
34	7	ad2antrr	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in A [\{x\}]) \to F : A ⟶ B$
35	22	adantl	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in A [\{x\}]) \to ⟨x, y⟩ \in A$
36	34 35	ffvelcdmd	$⊢ ((φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \land y \in A [\{x\}]) \to F (⟨x, y⟩) \in B$
37		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
38	37 7	fssdm	$⊢ φ \to F supp \underset{˙}{0} \subseteq A$
39	38	adantr	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to F supp \underset{˙}{0} \subseteq A$
40		imass1	$⊢ F supp \underset{˙}{0} \subseteq A \to {supp}_{\underset{˙}{0}} (F) [\{x\}] \subseteq A [\{x\}]$
41	39 40	syl	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to {supp}_{\underset{˙}{0}} (F) [\{x\}] \subseteq A [\{x\}]$
42	2 3 9 11 29 33 36 41	gsummptres2	$⊢ (φ \land x \in dom {supp}_{\underset{˙}{0}} (F)) \to \underset{y \in A [\{x\}]}{\sum_{W}} F (⟨x, y⟩) = \underset{y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]}{\sum_{W}} F (⟨x, y⟩)$
43	42	mpteq2dva	$⊢ φ \to (x \in dom {supp}_{\underset{˙}{0}} (F) ⟼ \underset{y \in A [\{x\}]}{\sum_{W}} F (⟨x, y⟩)) = (x \in dom {supp}_{\underset{˙}{0}} (F) ⟼ \underset{y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]}{\sum_{W}} F (⟨x, y⟩))$
44	43	oveq2d	$⊢ φ \to \underset{x \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{W}} (\underset{y \in A [\{x\}]}{\sum_{W}}, F (⟨x, y⟩)) = \underset{x \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{W}} (\underset{y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]}{\sum_{W}}, F (⟨x, y⟩))$
45	8	dmexd	$⊢ φ \to dom A \in V$
46	12	ad2antrr	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to F Fn A$
47	8	ad2antrr	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to A \in X$
48	15	a1i	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to \underset{˙}{0} \in V$
49	22	adantl	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to ⟨x, y⟩ \in A$
50		simplr	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))$
51	50	eldifbd	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to \neg x \in dom {supp}_{\underset{˙}{0}} (F)$
52	19 20	opeldm	$⊢ ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F) \to x \in dom {supp}_{\underset{˙}{0}} (F)$
53	51 52	nsyl	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to \neg ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F)$
54	49 53	eldifd	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to ⟨x, y⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))$
55	46 47 48 54	fvdifsupp	$⊢ ((φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \land y \in A [\{x\}]) \to F (⟨x, y⟩) = \underset{˙}{0}$
56	55	mpteq2dva	$⊢ (φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \to (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) = (y \in A [\{x\}] ⟼ \underset{˙}{0})$
57	56	oveq2d	$⊢ (φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \to \underset{y \in A [\{x\}]}{\sum_{W}} F (⟨x, y⟩) = \underset{y \in A [\{x\}]}{\sum_{W}} \underset{˙}{0}$
58	6	cmnmndd	$⊢ φ \to W \in Mnd$
59	8	adantr	$⊢ (φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \to A \in X$
60	59	imaexd	$⊢ (φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \to A [\{x\}] \in V$
61	3	gsumz	$⊢ (W \in Mnd \land A [\{x\}] \in V) \to \underset{y \in A [\{x\}]}{\sum_{W}} \underset{˙}{0} = \underset{˙}{0}$
62	58 60 61	syl2an2r	$⊢ (φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \to \underset{y \in A [\{x\}]}{\sum_{W}} \underset{˙}{0} = \underset{˙}{0}$
63	57 62	eqtrd	$⊢ (φ \land x \in (dom A ∖ dom {supp}_{\underset{˙}{0}} (F))) \to \underset{y \in A [\{x\}]}{\sum_{W}} F (⟨x, y⟩) = \underset{˙}{0}$
64		dmfi	$⊢ F supp \underset{˙}{0} \in Fin \to dom {supp}_{\underset{˙}{0}} (F) \in Fin$
65	30 64	syl	$⊢ φ \to dom {supp}_{\underset{˙}{0}} (F) \in Fin$
66	6	adantr	$⊢ (φ \land x \in dom A) \to W \in CMnd$
67	8	adantr	$⊢ (φ \land x \in dom A) \to A \in X$
68	67	imaexd	$⊢ (φ \land x \in dom A) \to A [\{x\}] \in V$
69	7	ad2antrr	$⊢ ((φ \land x \in dom A) \land y \in A [\{x\}]) \to F : A ⟶ B$
70	22	adantl	$⊢ ((φ \land x \in dom A) \land y \in A [\{x\}]) \to ⟨x, y⟩ \in A$
71	69 70	ffvelcdmd	$⊢ ((φ \land x \in dom A) \land y \in A [\{x\}]) \to F (⟨x, y⟩) \in B$
72	71	fmpttd	$⊢ (φ \land x \in dom A) \to (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) : A [\{x\}] ⟶ B$
73	68	mptexd	$⊢ (φ \land x \in dom A) \to (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) \in V$
74	72	ffnd	$⊢ (φ \land x \in dom A) \to (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) Fn A [\{x\}]$
75	15	a1i	$⊢ (φ \land x \in dom A) \to \underset{˙}{0} \in V$
76	30	adantr	$⊢ (φ \land x \in dom A) \to F supp \underset{˙}{0} \in Fin$
77	76 32	syl	$⊢ (φ \land x \in dom A) \to {supp}_{\underset{˙}{0}} (F) [\{x\}] \in Fin$
78		eqid	$⊢ (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) = (y \in A [\{x\}] ⟼ F (⟨x, y⟩))$
79		simp-4l	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to φ$
80		simp-4r	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to x \in dom A$
81		simpr	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to y = t$
82		simpllr	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to t \in A [\{x\}]$
83	81 82	eqeltrd	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to y \in A [\{x\}]$
84		simplr	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]$
85	81 84	eqneltrd	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]$
86	12	ad3antrrr	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to F Fn A$
87	8	ad3antrrr	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to A \in X$
88	15	a1i	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to \underset{˙}{0} \in V$
89	70	adantr	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to ⟨x, y⟩ \in A$
90	26	con3i	$⊢ \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}] \to \neg ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F)$
91	90	adantl	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to \neg ⟨x, y⟩ \in {supp}_{\underset{˙}{0}} (F)$
92	89 91	eldifd	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to ⟨x, y⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))$
93	86 87 88 92	fvdifsupp	$⊢ (((φ \land x \in dom A) \land y \in A [\{x\}]) \land \neg y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to F (⟨x, y⟩) = \underset{˙}{0}$
94	79 80 83 85 93	syl1111anc	$⊢ ((((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \land y = t) \to F (⟨x, y⟩) = \underset{˙}{0}$
95		simplr	$⊢ (((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to t \in A [\{x\}]$
96	15	a1i	$⊢ (((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to \underset{˙}{0} \in V$
97	78 94 95 96	fvmptd2	$⊢ (((φ \land x \in dom A) \land t \in A [\{x\}]) \land \neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}]) \to (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) (t) = \underset{˙}{0}$
98	97	ex	$⊢ ((φ \land x \in dom A) \land t \in A [\{x\}]) \to (\neg t \in {supp}_{\underset{˙}{0}} (F) [\{x\}] \to (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) (t) = \underset{˙}{0})$
99	98	orrd	$⊢ ((φ \land x \in dom A) \land t \in A [\{x\}]) \to (t \in {supp}_{\underset{˙}{0}} (F) [\{x\}] \lor (y \in A [\{x\}] ⟼ F (⟨x, y⟩)) (t) = \underset{˙}{0})$
100	73 74 75 77 99	finnzfsuppd	$⊢ (φ \land x \in dom A) \to {finSupp}_{\underset{˙}{0}} ((y \in A [\{x\}] ⟼ F (⟨x, y⟩)))$
101	2 3 66 68 72 100	gsumcl	$⊢ (φ \land x \in dom A) \to \underset{y \in A [\{x\}]}{\sum_{W}} F (⟨x, y⟩) \in B$
102		dmss	$⊢ F supp \underset{˙}{0} \subseteq A \to dom {supp}_{\underset{˙}{0}} (F) \subseteq dom A$
103	38 102	syl	$⊢ φ \to dom {supp}_{\underset{˙}{0}} (F) \subseteq dom A$
104	2 3 6 45 63 65 101 103	gsummptres2	$⊢ φ \to \underset{x \in dom A}{\sum_{W}} (\underset{y \in A [\{x\}]}{\sum_{W}}, F (⟨x, y⟩)) = \underset{x \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{W}} (\underset{y \in A [\{x\}]}{\sum_{W}}, F (⟨x, y⟩))$
105	7 38	feqresmpt	$⊢ φ \to {F ↾}_{{supp}_{\underset{˙}{0}} (F)} = (z \in {supp}_{\underset{˙}{0}} (F) ⟼ F (z))$
106	105	oveq2d	$⊢ φ \to \sum_{W} ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = \underset{z \in F supp \underset{˙}{0}}{\sum_{W}} F (z)$
107		ssidd	$⊢ φ \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
108	2 3 6 8 7 107 5	gsumres	$⊢ φ \to \sum_{W} ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = \sum_{W} F$
109		nfcv	$⊢ \underline{Ⅎ} y F (z)$
110		fveq2	$⊢ z = ⟨x, y⟩ \to F (z) = F (⟨x, y⟩)$
111		relss	$⊢ F supp \underset{˙}{0} \subseteq A \to (Rel A \to Rel {supp}_{\underset{˙}{0}} (F))$
112	38 4 111	sylc	$⊢ φ \to Rel {supp}_{\underset{˙}{0}} (F)$
113	7	adantr	$⊢ (φ \land z \in {supp}_{\underset{˙}{0}} (F)) \to F : A ⟶ B$
114	38	sselda	$⊢ (φ \land z \in {supp}_{\underset{˙}{0}} (F)) \to z \in A$
115	113 114	ffvelcdmd	$⊢ (φ \land z \in {supp}_{\underset{˙}{0}} (F)) \to F (z) \in B$
116	109 1 2 110 112 30 6 115	gsummpt2d	$⊢ φ \to \underset{z \in F supp \underset{˙}{0}}{\sum_{W}} F (z) = \underset{x \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{W}} (\underset{y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]}{\sum_{W}}, F (⟨x, y⟩))$
117	106 108 116	3eqtr3d	$⊢ φ \to \sum_{W} F = \underset{x \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{W}} (\underset{y \in {supp}_{\underset{˙}{0}} (F) [\{x\}]}{\sum_{W}}, F (⟨x, y⟩))$
118	44 104 117	3eqtr4rd	$⊢ φ \to \sum_{W} F = \underset{x \in dom A}{\sum_{W}} (\underset{y \in A [\{x\}]}{\sum_{W}}, F (⟨x, y⟩))$

Metamath Proof Explorer

Theorem gsumfs2d

Proof