Theorem 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	⊢ Ⅎ 𝑥 𝐻
	gsummptfsf1o.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptfsf1o.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptfsf1o.i	⊢ ( 𝑥 = 𝐸 → 𝐶 = 𝐻 )
	gsummptfsf1o.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptfsf1o.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsummptfsf1o.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) finSupp 0 )
	gsummptfsf1o.d	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
	gsummptfsf1o.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐹 )
	gsummptfsf1o.e	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐸 ∈ 𝐴 )
	gsummptfsf1o.h	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
Assertion	gsummptfsf1o	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfsf1o.x	⊢ Ⅎ 𝑥 𝐻
2		gsummptfsf1o.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		gsummptfsf1o.z	⊢ 0 = ( 0g ‘ 𝐺 )
4		gsummptfsf1o.i	⊢ ( 𝑥 = 𝐸 → 𝐶 = 𝐻 )
5		gsummptfsf1o.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
6		gsummptfsf1o.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7		gsummptfsf1o.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) finSupp 0 )
8		gsummptfsf1o.d	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
9		gsummptfsf1o.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐹 )
10		gsummptfsf1o.e	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐸 ∈ 𝐴 )
11		gsummptfsf1o.h	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
12	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ⊆ 𝐵 )
13	12 9	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
14	13	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
15	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐷 𝐸 ∈ 𝐴 )
16	11	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
17		eqid	⊢ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) = ( 𝑦 ∈ 𝐷 ↦ 𝐸 )
18	17	f1ompt	⊢ ( ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) : 𝐷 –1-1-onto→ 𝐴 ↔ ( ∀ 𝑦 ∈ 𝐷 𝐸 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 ) )
19	15 16 18	sylanbrc	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) : 𝐷 –1-1-onto→ 𝐴 )
20	2 3 5 6 14 7 19	gsumf1o	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) ) )
21		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) = ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) )
22		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
23	15 21 22	fmptcos	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) = ( 𝑦 ∈ 𝐷 ↦ ⦋ 𝐸 / 𝑥 ⦌ 𝐶 ) )
24		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐷 )
25	1	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → Ⅎ 𝑥 𝐻 )
26	4	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 = 𝐸 ) → 𝐶 = 𝐻 )
27	24 25 10 26	csbiedf	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ⦋ 𝐸 / 𝑥 ⦌ 𝐶 = 𝐻 )
28	27	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ⦋ 𝐸 / 𝑥 ⦌ 𝐶 ) = ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) )
29	23 28	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) = ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) )
30	29	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )
31	20 30	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )