Theorem gsuminv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 4-May-2015) (Revised by AV, 6-Jun-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 )
	gsuminv.a	|- ( ph -> A e. V )
	gsuminv.f	|- ( ph -> F : A --> B )
	gsuminv.n	|- ( ph -> F finSupp .0. )
Assertion	gsuminv	|- ( 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		gsuminv.a	|- ( ph -> A e. V )
6		gsuminv.f	|- ( ph -> F : A --> B )
7		gsuminv.n	|- ( ph -> F finSupp .0. )
8		ablcmn	|- ( G e. Abel -> G e. CMnd )
9	4 8	syl	|- ( ph -> G e. CMnd )
10		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
11	9 10	syl	|- ( ph -> G e. Mnd )
12	1 3	invghm	|- ( G e. Abel <-> I e. ( G GrpHom G ) )
13	4 12	sylib	|- ( ph -> I e. ( G GrpHom G ) )
14		ghmmhm	|- ( I e. ( G GrpHom G ) -> I e. ( G MndHom G ) )
15	13 14	syl	|- ( ph -> I e. ( G MndHom G ) )
16	1 2 9 11 5 15 6 7	gsummhm	|- ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )