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={\mathrm{Base}}_G$$
	gsuminv.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsuminv.p	$$⊢I={inv}_g\left(G\right)$$
	gsuminv.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	gsuminv.a	$$⊢\phi \to A\in V$$
	gsuminv.f	$$⊢\phi \to F:A⟶B$$
	gsuminv.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsuminv	$$⊢\phi \to {\sum }_G\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsuminv.b	$$⊢B={\mathrm{Base}}_G$$
2		gsuminv.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsuminv.p	$$⊢I={inv}_g\left(G\right)$$
4		gsuminv.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		gsuminv.a	$$⊢\phi \to A\in V$$
6		gsuminv.f	$$⊢\phi \to F:A⟶B$$
7		gsuminv.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
8		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
9	4 8	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
10		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
11	9 10	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
12	1 3	invghm	$$⊢G\in \mathrm{Abel}\leftrightarrow I\in \left(G\mathrm{GrpHom}G\right)$$
13	4 12	sylib	$$⊢\phi \to I\in \left(G\mathrm{GrpHom}G\right)$$
14		ghmmhm	$$⊢I\in \left(G\mathrm{GrpHom}G\right)\to I\in \left(G\mathrm{MndHom}G\right)$$
15	13 14	syl	$$⊢\phi \to I\in \left(G\mathrm{MndHom}G\right)$$
16	1 2 9 11 5 15 6 7	gsummhm	$$⊢\phi \to {\sum }_G\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$