gsumxp

Description: Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Hypotheses	gsumxp.b	$⊢ B = {Base}_{G}$
	gsumxp.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumxp.g	$⊢ φ \to G \in CMnd$
	gsumxp.a	$⊢ φ \to A \in V$
	gsumxp.r	$⊢ φ \to C \in W$
	gsumxp.f	$⊢ φ \to F : A \times C ⟶ B$
	gsumxp.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
Assertion	gsumxp	$⊢ φ \to \sum_{G} F = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, (j F k))$

Proof

Step	Hyp	Ref	Expression
1		gsumxp.b	$⊢ B = {Base}_{G}$
2		gsumxp.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumxp.g	$⊢ φ \to G \in CMnd$
4		gsumxp.a	$⊢ φ \to A \in V$
5		gsumxp.r	$⊢ φ \to C \in W$
6		gsumxp.f	$⊢ φ \to F : A \times C ⟶ B$
7		gsumxp.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8	4 5	xpexd	$⊢ φ \to A \times C \in V$
9		relxp	$⊢ Rel (A \times C)$
10	9	a1i	$⊢ φ \to Rel (A \times C)$
11		dmxpss	$⊢ dom (A \times C) \subseteq A$
12	11	a1i	$⊢ φ \to dom (A \times C) \subseteq A$
13	1 2 3 8 10 4 12 6 7	gsum2d	$⊢ φ \to \sum_{G} F = \underset{j \in A}{\sum_{G}} (\underset{k \in (A \times C) [\{j\}]}{\sum_{G}}, (j F k))$
14		df-ima	$⊢ (A \times C) [\{j\}] = ran ({(A \times C) ↾}_{\{j\}})$
15		df-res	$⊢ {(A \times C) ↾}_{\{j\}} = (A \times C) \cap (\{j\} \times V)$
16		inxp	$⊢ (A \times C) \cap (\{j\} \times V) = (A \cap \{j\}) \times (C \cap V)$
17	15 16	eqtri	$⊢ {(A \times C) ↾}_{\{j\}} = (A \cap \{j\}) \times (C \cap V)$
18		simpr	$⊢ (φ \land j \in A) \to j \in A$
19	18	snssd	$⊢ (φ \land j \in A) \to \{j\} \subseteq A$
20		sseqin2	$⊢ \{j\} \subseteq A \leftrightarrow A \cap \{j\} = \{j\}$
21	19 20	sylib	$⊢ (φ \land j \in A) \to A \cap \{j\} = \{j\}$
22		inv1	$⊢ C \cap V = C$
23	22	a1i	$⊢ (φ \land j \in A) \to C \cap V = C$
24	21 23	xpeq12d	$⊢ (φ \land j \in A) \to (A \cap \{j\}) \times (C \cap V) = \{j\} \times C$
25	17 24	syl5eq	$⊢ (φ \land j \in A) \to {(A \times C) ↾}_{\{j\}} = \{j\} \times C$
26	25	rneqd	$⊢ (φ \land j \in A) \to ran ({(A \times C) ↾}_{\{j\}}) = ran (\{j\} \times C)$
27		vex	$⊢ j \in V$
28	27	snnz	$⊢ \{j\} \neq \emptyset$
29		rnxp	$⊢ \{j\} \neq \emptyset \to ran (\{j\} \times C) = C$
30	28 29	ax-mp	$⊢ ran (\{j\} \times C) = C$
31	26 30	eqtrdi	$⊢ (φ \land j \in A) \to ran ({(A \times C) ↾}_{\{j\}}) = C$
32	14 31	syl5eq	$⊢ (φ \land j \in A) \to (A \times C) [\{j\}] = C$
33	32	mpteq1d	$⊢ (φ \land j \in A) \to (k \in (A \times C) [\{j\}] ⟼ j F k) = (k \in C ⟼ j F k)$
34	33	oveq2d	$⊢ (φ \land j \in A) \to \underset{k \in (A \times C) [\{j\}]}{\sum_{G}} (j F k) = \underset{k \in C}{\sum_{G}} (j F k)$
35	34	mpteq2dva	$⊢ φ \to (j \in A ⟼ \underset{k \in (A \times C) [\{j\}]}{\sum_{G}} (j F k)) = (j \in A ⟼ \underset{k \in C}{\sum_{G}} (j F k))$
36	35	oveq2d	$⊢ φ \to \underset{j \in A}{\sum_{G}} (\underset{k \in (A \times C) [\{j\}]}{\sum_{G}}, (j F k)) = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, (j F k))$
37	13 36	eqtrd	$⊢ φ \to \sum_{G} F = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, (j F k))$

Metamath Proof Explorer

Theorem gsumxp

Proof