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={\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}$$
	gsummptfidminv.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsummptfidminv.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	gsummptfidminv.f	$$⊢F=\left(x\in A⟼C\right)$$
Assertion	gsummptfidminv	$$⊢\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		gsummptfidminv.a	$$⊢\phi \to A\in \mathrm{Fin}$$
6		gsummptfidminv.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
7		gsummptfidminv.f	$$⊢F=\left(x\in A⟼C\right)$$
8	6 7	fmptd	$$⊢\phi \to F:A⟶B$$
9	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
11	7 5 6 10	fsuppmptdm	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
12	1 2 3 4 5 8 11	gsuminv	$$⊢\phi \to {\sum }_G\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$