Theorem gsummptfidminv

Description: Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsuminv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsuminv.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsuminv.p	⊢ 𝐼 = ( invg ‘ 𝐺 )
	gsuminv.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	gsummptfidminv.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummptfidminv.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	gsummptfidminv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion	gsummptfidminv	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsuminv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsuminv.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsuminv.p	⊢ 𝐼 = ( invg ‘ 𝐺 )
4		gsuminv.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
5		gsummptfidminv.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
6		gsummptfidminv.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
7		gsummptfidminv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
8	6 7	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9	2	fvexi	⊢ 0 ∈ V
10	9	a1i	⊢ ( 𝜑 → 0 ∈ V )
11	7 5 6 10	fsuppmptdm	⊢ ( 𝜑 → 𝐹 finSupp 0 )
12	1 2 3 4 5 8 11	gsuminv	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )