Theorem gsummptf1od

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

	Ref	Expression
Hypotheses	gsummptf1od.x	⊢ Ⅎ 𝑥 𝐻
	gsummptf1od.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptf1od.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptf1od.i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 = 𝐸 ) → 𝐶 = 𝐻 )
	gsummptf1od.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptf1od.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummptf1od.d	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
	gsummptf1od.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐹 )
	gsummptf1od.e	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐸 ∈ 𝐴 )
	gsummptf1od.h	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
Assertion	gsummptf1od	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )

Proof

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