gsumxp2

Description: Write a group sum over a cartesian product as a double sum in two ways. This corresponds to the first equation in Lang p. 6. (Contributed by AV, 27-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		gsumxp2.b	$⊢ B = {Base}_{G}$
2		gsumxp2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumxp2.g	$⊢ φ \to G \in CMnd$
4		gsumxp2.a	$⊢ φ \to A \in V$
5		gsumxp2.r	$⊢ φ \to C \in W$
6		gsumxp2.f	$⊢ φ \to F : A \times C ⟶ B$
7		gsumxp2.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8	6	fovcdmda	$⊢ (φ \land (j \in A \land k \in C)) \to j F k \in B$
9	7	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
10		simpl	$⊢ (φ \land (j \in A \land k \in C)) \to φ$
11		opelxpi	$⊢ (j \in A \land k \in C) \to ⟨j, k⟩ \in (A \times C)$
12	11	ad2antlr	$⊢ ((φ \land (j \in A \land k \in C)) \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)) \to ⟨j, k⟩ \in (A \times C)$
13		simpr	$⊢ ((φ \land (j \in A \land k \in C)) \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)) \to \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)$
14	12 13	eldifd	$⊢ ((φ \land (j \in A \land k \in C)) \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)) \to ⟨j, k⟩ \in ((A \times C) ∖ {supp}_{\underset{˙}{0}} (F))$
15		ssidd	$⊢ φ \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
16	4 5	xpexd	$⊢ φ \to A \times C \in V$
17	2	fvexi	$⊢ \underset{˙}{0} \in V$
18	17	a1i	$⊢ φ \to \underset{˙}{0} \in V$
19	6 15 16 18	suppssr	$⊢ (φ \land ⟨j, k⟩ \in ((A \times C) ∖ {supp}_{\underset{˙}{0}} (F))) \to F (⟨j, k⟩) = \underset{˙}{0}$
20	10 14 19	syl2an2r	$⊢ ((φ \land (j \in A \land k \in C)) \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)) \to F (⟨j, k⟩) = \underset{˙}{0}$
21	20	ex	$⊢ (φ \land (j \in A \land k \in C)) \to (\neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F) \to F (⟨j, k⟩) = \underset{˙}{0})$
22		df-br	$⊢ j {supp}_{\underset{˙}{0}} (F) k \leftrightarrow ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)$
23	22	notbii	$⊢ \neg j {supp}_{\underset{˙}{0}} (F) k \leftrightarrow \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)$
24		df-ov	$⊢ j F k = F (⟨j, k⟩)$
25	24	eqeq1i	$⊢ j F k = \underset{˙}{0} \leftrightarrow F (⟨j, k⟩) = \underset{˙}{0}$
26	21 23 25	3imtr4g	$⊢ (φ \land (j \in A \land k \in C)) \to (\neg j {supp}_{\underset{˙}{0}} (F) k \to j F k = \underset{˙}{0})$
27	26	impr	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j {supp}_{\underset{˙}{0}} (F) k)) \to j F k = \underset{˙}{0}$
28	1 2 3 4 5 8 9 27	gsumcom3	$⊢ φ \to \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, (j F k)) = \underset{k \in C}{\sum_{G}} (\underset{j \in A}{\sum_{G}}, (j F k))$
29	28	eqcomd	$⊢ φ \to \underset{k \in C}{\sum_{G}} (\underset{j \in A}{\sum_{G}}, (j F k)) = \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, (j F k))$

Metamath Proof Explorer

Theorem gsumxp2

Proof