gsummptf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018)

	Ref	Expression
Hypotheses	gsummptf1o.x	$⊢ \underline{Ⅎ} x H$
	gsummptf1o.b	$⊢ B = {Base}_{G}$
	gsummptf1o.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsummptf1o.i	$⊢ x = E \to C = H$
	gsummptf1o.g	$⊢ φ \to G \in CMnd$
	gsummptf1o.a	$⊢ φ \to A \in Fin$
	gsummptf1o.d	$⊢ φ \to F \subseteq B$
	gsummptf1o.f	$⊢ (φ \land x \in A) \to C \in F$
	gsummptf1o.e	$⊢ (φ \land y \in D) \to E \in A$
	gsummptf1o.h	$⊢ (φ \land x \in A) \to \exists! y \in D x = E$
Assertion	gsummptf1o	$⊢ φ \to \underset{x \in A}{\sum_{G}} C = \underset{y \in D}{\sum_{G}} H$

Proof

Step	Hyp	Ref	Expression
1		gsummptf1o.x	$⊢ \underline{Ⅎ} x H$
2		gsummptf1o.b	$⊢ B = {Base}_{G}$
3		gsummptf1o.z	$⊢ \underset{˙}{0} = 0_{G}$
4		gsummptf1o.i	$⊢ x = E \to C = H$
5		gsummptf1o.g	$⊢ φ \to G \in CMnd$
6		gsummptf1o.a	$⊢ φ \to A \in Fin$
7		gsummptf1o.d	$⊢ φ \to F \subseteq B$
8		gsummptf1o.f	$⊢ (φ \land x \in A) \to C \in F$
9		gsummptf1o.e	$⊢ (φ \land y \in D) \to E \in A$
10		gsummptf1o.h	$⊢ (φ \land x \in A) \to \exists! y \in D x = E$
11	7	adantr	$⊢ (φ \land x \in A) \to F \subseteq B$
12	11 8	sseldd	$⊢ (φ \land x \in A) \to C \in B$
13	12	fmpttd	$⊢ φ \to (x \in A ⟼ C) : A ⟶ B$
14		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
15	3	fvexi	$⊢ \underset{˙}{0} \in V$
16	15	a1i	$⊢ φ \to \underset{˙}{0} \in V$
17	14 6 12 16	fsuppmptdm	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ C))$
18	9	ralrimiva	$⊢ φ \to \forall y \in D E \in A$
19	10	ralrimiva	$⊢ φ \to \forall x \in A \exists! y \in D x = E$
20		eqid	$⊢ (y \in D ⟼ E) = (y \in D ⟼ E)$
21	20	f1ompt	$⊢ (y \in D ⟼ E) : D \underset{1-1 onto}{⟶} A \leftrightarrow (\forall y \in D E \in A \land \forall x \in A \exists! y \in D x = E)$
22	18 19 21	sylanbrc	$⊢ φ \to (y \in D ⟼ E) : D \underset{1-1 onto}{⟶} A$
23	2 3 5 6 13 17 22	gsumf1o	$⊢ φ \to \underset{x \in A}{\sum_{G}} C = \sum_{G} ((x \in A ⟼ C) \circ (y \in D ⟼ E))$
24		eqidd	$⊢ φ \to (y \in D ⟼ E) = (y \in D ⟼ E)$
25		eqidd	$⊢ φ \to (x \in A ⟼ C) = (x \in A ⟼ C)$
26	18 24 25	fmptcos	$⊢ φ \to (x \in A ⟼ C) \circ (y \in D ⟼ E) = (y \in D ⟼ ⦋ E / x ⦌ C)$
27		nfv	$⊢ Ⅎ x (φ \land y \in D)$
28	1	a1i	$⊢ (φ \land y \in D) \to \underline{Ⅎ} x H$
29	4	adantl	$⊢ ((φ \land y \in D) \land x = E) \to C = H$
30	27 28 9 29	csbiedf	$⊢ (φ \land y \in D) \to ⦋ E / x ⦌ C = H$
31	30	mpteq2dva	$⊢ φ \to (y \in D ⟼ ⦋ E / x ⦌ C) = (y \in D ⟼ H)$
32	26 31	eqtrd	$⊢ φ \to (x \in A ⟼ C) \circ (y \in D ⟼ E) = (y \in D ⟼ H)$
33	32	oveq2d	$⊢ φ \to \sum_{G} ((x \in A ⟼ C) \circ (y \in D ⟼ E)) = \underset{y \in D}{\sum_{G}} H$
34	23 33	eqtrd	$⊢ φ \to \underset{x \in A}{\sum_{G}} C = \underset{y \in D}{\sum_{G}} H$

Metamath Proof Explorer

Theorem gsummptf1o

Proof