gsumpart

Description: Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024)

	Ref	Expression
Hypotheses	gsumpart.b	$⊢ B = {Base}_{G}$
	gsumpart.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumpart.g	$⊢ φ \to G \in CMnd$
	gsumpart.a	$⊢ φ \to A \in V$
	gsumpart.x	$⊢ φ \to X \in W$
	gsumpart.f	$⊢ φ \to F : A ⟶ B$
	gsumpart.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumpart.1	$⊢ φ \to \underset{x \in X}{Disj} C$
	gsumpart.2	$⊢ φ \to ⋃_{x \in X} C = A$
Assertion	gsumpart	$⊢ φ \to \sum_{G} F = \underset{x \in X}{\sum_{G}} (\sum_{G}, ({F ↾}_{C}))$

Proof

Step	Hyp	Ref	Expression
1		gsumpart.b	$⊢ B = {Base}_{G}$
2		gsumpart.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumpart.g	$⊢ φ \to G \in CMnd$
4		gsumpart.a	$⊢ φ \to A \in V$
5		gsumpart.x	$⊢ φ \to X \in W$
6		gsumpart.f	$⊢ φ \to F : A ⟶ B$
7		gsumpart.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		gsumpart.1	$⊢ φ \to \underset{x \in X}{Disj} C$
9		gsumpart.2	$⊢ φ \to ⋃_{x \in X} C = A$
10		eqid	$⊢ ⋃_{x \in X} (\{x\} \times C) = ⋃_{x \in X} (\{x\} \times C)$
11	10 4 5 8 9	2ndresdjuf1o	$⊢ φ \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) \underset{1-1 onto}{⟶} A$
12	1 2 3 4 6 7 11	gsumf1o	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}))$
13		snex	$⊢ \{x\} \in V$
14	13	a1i	$⊢ (φ \land x \in X) \to \{x\} \in V$
15	4	adantr	$⊢ (φ \land x \in X) \to A \in V$
16		ssidd	$⊢ φ \to A \subseteq A$
17	9 16	eqsstrd	$⊢ φ \to ⋃_{x \in X} C \subseteq A$
18		iunss	$⊢ ⋃_{x \in X} C \subseteq A \leftrightarrow \forall x \in X C \subseteq A$
19	17 18	sylib	$⊢ φ \to \forall x \in X C \subseteq A$
20	19	r19.21bi	$⊢ (φ \land x \in X) \to C \subseteq A$
21	15 20	ssexd	$⊢ (φ \land x \in X) \to C \in V$
22	14 21	xpexd	$⊢ (φ \land x \in X) \to \{x\} \times C \in V$
23	22	ralrimiva	$⊢ φ \to \forall x \in X \{x\} \times C \in V$
24		iunexg	$⊢ (X \in W \land \forall x \in X \{x\} \times C \in V) \to ⋃_{x \in X} (\{x\} \times C) \in V$
25	5 23 24	syl2anc	$⊢ φ \to ⋃_{x \in X} (\{x\} \times C) \in V$
26		relxp	$⊢ Rel (\{x\} \times C)$
27	26	a1i	$⊢ (φ \land x \in X) \to Rel (\{x\} \times C)$
28	27	ralrimiva	$⊢ φ \to \forall x \in X Rel (\{x\} \times C)$
29		reliun	$⊢ Rel ⋃_{x \in X} (\{x\} \times C) \leftrightarrow \forall x \in X Rel (\{x\} \times C)$
30	28 29	sylibr	$⊢ φ \to Rel ⋃_{x \in X} (\{x\} \times C)$
31		dmiun	$⊢ dom ⋃_{x \in X} (\{x\} \times C) = ⋃_{x \in X} dom (\{x\} \times C)$
32		dmxpss	$⊢ dom (\{x\} \times C) \subseteq \{x\}$
33	32	rgenw	$⊢ \forall x \in X dom (\{x\} \times C) \subseteq \{x\}$
34		ss2iun	$⊢ \forall x \in X dom (\{x\} \times C) \subseteq \{x\} \to ⋃_{x \in X} dom (\{x\} \times C) \subseteq ⋃_{x \in X} \{x\}$
35	33 34	ax-mp	$⊢ ⋃_{x \in X} dom (\{x\} \times C) \subseteq ⋃_{x \in X} \{x\}$
36	31 35	eqsstri	$⊢ dom ⋃_{x \in X} (\{x\} \times C) \subseteq ⋃_{x \in X} \{x\}$
37		iunid	$⊢ ⋃_{x \in X} \{x\} = X$
38	36 37	sseqtri	$⊢ dom ⋃_{x \in X} (\{x\} \times C) \subseteq X$
39	38	a1i	$⊢ φ \to dom ⋃_{x \in X} (\{x\} \times C) \subseteq X$
40		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
41		fof	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} : V ⟶ V$
42	40 41	ax-mp	$⊢ 2^{nd} : V ⟶ V$
43		ssv	$⊢ ⋃_{x \in X} (\{x\} \times C) \subseteq V$
44		fssres	$⊢ (2^{nd} : V ⟶ V \land ⋃_{x \in X} (\{x\} \times C) \subseteq V) \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) ⟶ V$
45	42 43 44	mp2an	$⊢ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) ⟶ V$
46		ffn	$⊢ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) ⟶ V \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) Fn ⋃_{x \in X} (\{x\} \times C)$
47	45 46	mp1i	$⊢ φ \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) Fn ⋃_{x \in X} (\{x\} \times C)$
48		djussxp2	$⊢ ⋃_{x \in X} (\{x\} \times C) \subseteq X \times ⋃_{x \in X} C$
49		imass2	$⊢ ⋃_{x \in X} (\{x\} \times C) \subseteq X \times ⋃_{x \in X} C \to 2^{nd} [⋃_{x \in X} (\{x\} \times C)] \subseteq 2^{nd} [X \times ⋃_{x \in X} C]$
50	48 49	ax-mp	$⊢ 2^{nd} [⋃_{x \in X} (\{x\} \times C)] \subseteq 2^{nd} [X \times ⋃_{x \in X} C]$
51		ima0	$⊢ 2^{nd} [\emptyset] = \emptyset$
52		xpeq1	$⊢ X = \emptyset \to X \times ⋃_{x \in X} C = \emptyset \times ⋃_{x \in X} C$
53		0xp	$⊢ \emptyset \times ⋃_{x \in X} C = \emptyset$
54	52 53	eqtrdi	$⊢ X = \emptyset \to X \times ⋃_{x \in X} C = \emptyset$
55	54	imaeq2d	$⊢ X = \emptyset \to 2^{nd} [X \times ⋃_{x \in X} C] = 2^{nd} [\emptyset]$
56		iuneq1	$⊢ X = \emptyset \to ⋃_{x \in X} C = ⋃_{x \in \emptyset} C$
57		0iun	$⊢ ⋃_{x \in \emptyset} C = \emptyset$
58	56 57	eqtrdi	$⊢ X = \emptyset \to ⋃_{x \in X} C = \emptyset$
59	51 55 58	3eqtr4a	$⊢ X = \emptyset \to 2^{nd} [X \times ⋃_{x \in X} C] = ⋃_{x \in X} C$
60	59	adantl	$⊢ (φ \land X = \emptyset) \to 2^{nd} [X \times ⋃_{x \in X} C] = ⋃_{x \in X} C$
61		2ndimaxp	$⊢ X \neq \emptyset \to 2^{nd} [X \times ⋃_{x \in X} C] = ⋃_{x \in X} C$
62	61	adantl	$⊢ (φ \land X \neq \emptyset) \to 2^{nd} [X \times ⋃_{x \in X} C] = ⋃_{x \in X} C$
63	60 62	pm2.61dane	$⊢ φ \to 2^{nd} [X \times ⋃_{x \in X} C] = ⋃_{x \in X} C$
64	63 9	eqtrd	$⊢ φ \to 2^{nd} [X \times ⋃_{x \in X} C] = A$
65	50 64	sseqtrid	$⊢ φ \to 2^{nd} [⋃_{x \in X} (\{x\} \times C)] \subseteq A$
66		resssxp	$⊢ 2^{nd} [⋃_{x \in X} (\{x\} \times C)] \subseteq A \leftrightarrow {2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)} \subseteq ⋃_{x \in X} (\{x\} \times C) \times A$
67	65 66	sylib	$⊢ φ \to {2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)} \subseteq ⋃_{x \in X} (\{x\} \times C) \times A$
68		dff2	$⊢ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) ⟶ A \leftrightarrow (({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) Fn ⋃_{x \in X} (\{x\} \times C) \land {2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)} \subseteq ⋃_{x \in X} (\{x\} \times C) \times A)$
69	47 67 68	sylanbrc	$⊢ φ \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) ⟶ A$
70	6 69	fcod	$⊢ φ \to (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) : ⋃_{x \in X} (\{x\} \times C) ⟶ B$
71	10 4 5 8 9	2ndresdju	$⊢ φ \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) \underset{1-1}{⟶} A$
72	2	fvexi	$⊢ \underset{˙}{0} \in V$
73	72	a1i	$⊢ φ \to \underset{˙}{0} \in V$
74	6 4	fexd	$⊢ φ \to F \in V$
75	7 71 73 74	fsuppco	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})))$
76	1 2 3 25 30 5 39 70 75	gsum2d	$⊢ φ \to \sum_{G} (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) = \underset{y \in X}{\sum_{G}} (\underset{z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]}{\sum_{G}}, (y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z))$
77		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ C$
78		csbeq1a	$⊢ x = y \to C = ⦋ y / x ⦌ C$
79	5 21 77 78	iunsnima2	$⊢ (φ \land y \in X) \to ⋃_{x \in X} (\{x\} \times C) [\{y\}] = ⦋ y / x ⦌ C$
80		df-ov	$⊢ y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z = (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) (⟨y, z⟩)$
81	69	ad2antrr	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) : ⋃_{x \in X} (\{x\} \times C) ⟶ A$
82		simplr	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to y \in X$
83		vsnid	$⊢ y \in \{y\}$
84	83	a1i	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to y \in \{y\}$
85	79	eleq2d	$⊢ (φ \land y \in X) \to (z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}] \leftrightarrow z \in ⦋ y / x ⦌ C)$
86	85	biimpa	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to z \in ⦋ y / x ⦌ C$
87	84 86	opelxpd	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to ⟨y, z⟩ \in (\{y\} \times ⦋ y / x ⦌ C)$
88		nfcv	$⊢ \underline{Ⅎ} x \{y\}$
89	88 77	nfxp	$⊢ \underline{Ⅎ} x (\{y\} \times ⦋ y / x ⦌ C)$
90	89	nfel2	$⊢ Ⅎ x ⟨y, z⟩ \in (\{y\} \times ⦋ y / x ⦌ C)$
91		sneq	$⊢ x = y \to \{x\} = \{y\}$
92	91 78	xpeq12d	$⊢ x = y \to \{x\} \times C = \{y\} \times ⦋ y / x ⦌ C$
93	92	eleq2d	$⊢ x = y \to (⟨y, z⟩ \in (\{x\} \times C) \leftrightarrow ⟨y, z⟩ \in (\{y\} \times ⦋ y / x ⦌ C))$
94	90 93	rspce	$⊢ (y \in X \land ⟨y, z⟩ \in (\{y\} \times ⦋ y / x ⦌ C)) \to \exists x \in X ⟨y, z⟩ \in (\{x\} \times C)$
95	82 87 94	syl2anc	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to \exists x \in X ⟨y, z⟩ \in (\{x\} \times C)$
96		eliun	$⊢ ⟨y, z⟩ \in ⋃_{x \in X} (\{x\} \times C) \leftrightarrow \exists x \in X ⟨y, z⟩ \in (\{x\} \times C)$
97	95 96	sylibr	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to ⟨y, z⟩ \in ⋃_{x \in X} (\{x\} \times C)$
98	81 97	fvco3d	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) (⟨y, z⟩) = F (({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) (⟨y, z⟩))$
99	97	fvresd	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) (⟨y, z⟩) = 2^{nd} (⟨y, z⟩)$
100		vex	$⊢ y \in V$
101		vex	$⊢ z \in V$
102	100 101	op2nd	$⊢ 2^{nd} (⟨y, z⟩) = z$
103	99 102	eqtrdi	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) (⟨y, z⟩) = z$
104	103	fveq2d	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to F (({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)}) (⟨y, z⟩)) = F (z)$
105	98 104	eqtrd	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) (⟨y, z⟩) = F (z)$
106	80 105	syl5eq	$⊢ ((φ \land y \in X) \land z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]) \to y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z = F (z)$
107	79 106	mpteq12dva	$⊢ (φ \land y \in X) \to (z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}] ⟼ y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z) = (z \in ⦋ y / x ⦌ C ⟼ F (z))$
108	6	adantr	$⊢ (φ \land y \in X) \to F : A ⟶ B$
109		imassrn	$⊢ ⋃_{x \in X} (\{x\} \times C) [\{y\}] \subseteq ran ⋃_{x \in X} (\{x\} \times C)$
110	9	xpeq2d	$⊢ φ \to X \times ⋃_{x \in X} C = X \times A$
111	48 110	sseqtrid	$⊢ φ \to ⋃_{x \in X} (\{x\} \times C) \subseteq X \times A$
112		rnss	$⊢ ⋃_{x \in X} (\{x\} \times C) \subseteq X \times A \to ran ⋃_{x \in X} (\{x\} \times C) \subseteq ran (X \times A)$
113	111 112	syl	$⊢ φ \to ran ⋃_{x \in X} (\{x\} \times C) \subseteq ran (X \times A)$
114	113	adantr	$⊢ (φ \land y \in X) \to ran ⋃_{x \in X} (\{x\} \times C) \subseteq ran (X \times A)$
115		rnxpss	$⊢ ran (X \times A) \subseteq A$
116	114 115	sstrdi	$⊢ (φ \land y \in X) \to ran ⋃_{x \in X} (\{x\} \times C) \subseteq A$
117	109 116	sstrid	$⊢ (φ \land y \in X) \to ⋃_{x \in X} (\{x\} \times C) [\{y\}] \subseteq A$
118	79 117	eqsstrrd	$⊢ (φ \land y \in X) \to ⦋ y / x ⦌ C \subseteq A$
119	108 118	feqresmpt	$⊢ (φ \land y \in X) \to {F ↾}_{⦋ y / x ⦌ C} = (z \in ⦋ y / x ⦌ C ⟼ F (z))$
120	107 119	eqtr4d	$⊢ (φ \land y \in X) \to (z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}] ⟼ y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z) = {F ↾}_{⦋ y / x ⦌ C}$
121	120	oveq2d	$⊢ (φ \land y \in X) \to \underset{z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]}{\sum_{G}} (y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z) = \sum_{G} ({F ↾}_{⦋ y / x ⦌ C})$
122	121	mpteq2dva	$⊢ φ \to (y \in X ⟼ \underset{z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]}{\sum_{G}} (y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z)) = (y \in X ⟼ \sum_{G} ({F ↾}_{⦋ y / x ⦌ C}))$
123		nfcv	$⊢ \underline{Ⅎ} y (\sum_{G}, ({F ↾}_{C}))$
124		nfcv	$⊢ \underline{Ⅎ} x G$
125		nfcv	$⊢ \underline{Ⅎ} x Σ_{𝑔}$
126		nfcv	$⊢ \underline{Ⅎ} x F$
127	126 77	nfres	$⊢ \underline{Ⅎ} x ({F ↾}_{⦋ y / x ⦌ C})$
128	124 125 127	nfov	$⊢ \underline{Ⅎ} x (\sum_{G}, ({F ↾}_{⦋ y / x ⦌ C}))$
129	78	reseq2d	$⊢ x = y \to {F ↾}_{C} = {F ↾}_{⦋ y / x ⦌ C}$
130	129	oveq2d	$⊢ x = y \to \sum_{G} ({F ↾}_{C}) = \sum_{G} ({F ↾}_{⦋ y / x ⦌ C})$
131	123 128 130	cbvmpt	$⊢ (x \in X ⟼ \sum_{G} ({F ↾}_{C})) = (y \in X ⟼ \sum_{G} ({F ↾}_{⦋ y / x ⦌ C}))$
132	122 131	eqtr4di	$⊢ φ \to (y \in X ⟼ \underset{z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]}{\sum_{G}} (y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z)) = (x \in X ⟼ \sum_{G} ({F ↾}_{C}))$
133	132	oveq2d	$⊢ φ \to \underset{y \in X}{\sum_{G}} (\underset{z \in ⋃_{x \in X} (\{x\} \times C) [\{y\}]}{\sum_{G}}, (y (F \circ ({2^{nd} ↾}_{⋃_{x \in X} (\{x\} \times C)})) z)) = \underset{x \in X}{\sum_{G}} (\sum_{G}, ({F ↾}_{C}))$
134	12 76 133	3eqtrd	$⊢ φ \to \sum_{G} F = \underset{x \in X}{\sum_{G}} (\sum_{G}, ({F ↾}_{C}))$

Metamath Proof Explorer

Theorem gsumpart

Proof