gsummptfsf1o

Description: Re-index a finite group sum using a bijection. A version of gsummptf1o expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025)

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

Proof

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

Metamath Proof Explorer

Theorem gsummptfsf1o

Proof