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	|- B = ( Base ` G )
	gsuminv.z	|- .0. = ( 0g ` G )
	gsuminv.p	|- I = ( invg ` G )
	gsuminv.g	|- ( ph -> G e. Abel )
	gsummptfidminv.a	|- ( ph -> A e. Fin )
	gsummptfidminv.c	|- ( ( ph /\ x e. A ) -> C e. B )
	gsummptfidminv.f	|- F = ( x e. A |-> C )
Assertion	gsummptfidminv	|- ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsuminv.b	|- B = ( Base ` G )
2		gsuminv.z	|- .0. = ( 0g ` G )
3		gsuminv.p	|- I = ( invg ` G )
4		gsuminv.g	|- ( ph -> G e. Abel )
5		gsummptfidminv.a	|- ( ph -> A e. Fin )
6		gsummptfidminv.c	|- ( ( ph /\ x e. A ) -> C e. B )
7		gsummptfidminv.f	|- F = ( x e. A |-> C )
8	6 7	fmptd	|- ( ph -> F : A --> B )
9	2	fvexi	|- .0. e. _V
10	9	a1i	|- ( ph -> .0. e. _V )
11	7 5 6 10	fsuppmptdm	|- ( ph -> F finSupp .0. )
12	1 2 3 4 5 8 11	gsuminv	|- ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )