Theorem gsumzinv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsumzinv.b	$$⊢B={\mathrm{Base}}_G$$
	gsumzinv.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumzinv.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzinv.i	$$⊢I={inv}_g\left(G\right)$$
	gsumzinv.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	gsumzinv.a	$$⊢\phi \to A\in V$$
	gsumzinv.f	$$⊢\phi \to F:A⟶B$$
	gsumzinv.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumzinv.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumzinv	$$⊢\phi \to {\sum }_G\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumzinv.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumzinv.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumzinv.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
4		gsumzinv.i	$$⊢I={inv}_g\left(G\right)$$
5		gsumzinv.g	$$⊢\phi \to G\in \mathrm{Grp}$$
6		gsumzinv.a	$$⊢\phi \to A\in V$$
7		gsumzinv.f	$$⊢\phi \to F:A⟶B$$
8		gsumzinv.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
9		gsumzinv.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
10		eqid	$$⊢{opp}_{𝑔}\left(G\right)={opp}_{𝑔}\left(G\right)$$
11	5	grpmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
12	1 4	grpinvf	$$⊢G\in \mathrm{Grp}\to I:B⟶B$$
13	5 12	syl	$$⊢\phi \to I:B⟶B$$
14		fco	$$⊢\left(I:B⟶B\wedge F:A⟶B\right)\to \left(I\circ F\right):A⟶B$$
15	13 7 14	syl2anc	$$⊢\phi \to \left(I\circ F\right):A⟶B$$
16	10 4	invoppggim	$$⊢G\in \mathrm{Grp}\to I\in \left(G\mathrm{GrpIso}{opp}_{𝑔}\left(G\right)\right)$$
17		gimghm	$$⊢I\in \left(G\mathrm{GrpIso}{opp}_{𝑔}\left(G\right)\right)\to I\in \left(G\mathrm{GrpHom}{opp}_{𝑔}\left(G\right)\right)$$
18		ghmmhm	$$⊢I\in \left(G\mathrm{GrpHom}{opp}_{𝑔}\left(G\right)\right)\to I\in \left(G\mathrm{MndHom}{opp}_{𝑔}\left(G\right)\right)$$
19	5 16 17 18	4syl	$$⊢\phi \to I\in \left(G\mathrm{MndHom}{opp}_{𝑔}\left(G\right)\right)$$
20		eqid	$$⊢\mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)=\mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)$$
21	3 20	cntzmhm2	$$⊢\left(I\in \left(G\mathrm{MndHom}{opp}_{𝑔}\left(G\right)\right)\wedge \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)\right)\to I\left[\mathrm{ran}F\right]\subseteq \mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)\left(I\left[\mathrm{ran}F\right]\right)$$
22	19 8 21	syl2anc	$$⊢\phi \to I\left[\mathrm{ran}F\right]\subseteq \mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)\left(I\left[\mathrm{ran}F\right]\right)$$
23		rnco2	$$⊢\mathrm{ran}\left(I\circ F\right)=I\left[\mathrm{ran}F\right]$$
24	23	fveq2i	$$⊢Z\left(\mathrm{ran}\left(I\circ F\right)\right)=Z\left(I\left[\mathrm{ran}F\right]\right)$$
25	10 3	oppgcntz	$$⊢Z\left(I\left[\mathrm{ran}F\right]\right)=\mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)\left(I\left[\mathrm{ran}F\right]\right)$$
26	24 25	eqtri	$$⊢Z\left(\mathrm{ran}\left(I\circ F\right)\right)=\mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)\left(I\left[\mathrm{ran}F\right]\right)$$
27	22 23 26	3sstr4g	$$⊢\phi \to \mathrm{ran}\left(I\circ F\right)\subseteq Z\left(\mathrm{ran}\left(I\circ F\right)\right)$$
28	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
29	28	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
30	1	fvexi	$$⊢B\in \mathrm{V}$$
31	30	a1i	$$⊢\phi \to B\in \mathrm{V}$$
32	2 4	grpinvid	$$⊢G\in \mathrm{Grp}\to I\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
33	5 32	syl	$$⊢\phi \to I\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
34	29 7 13 6 31 9 33	fsuppco2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(I\circ F\right)\right)$$
35	1 2 3 10 11 6 15 27 34	gsumzoppg	$$⊢\phi \to {\sum }_{{opp}_{𝑔}\left(G\right)}\left(I\circ F\right)={\sum }_G\left(I\circ F\right)$$
36	10	oppgmnd	$$⊢G\in \mathrm{Mnd}\to {opp}_{𝑔}\left(G\right)\in \mathrm{Mnd}$$
37	11 36	syl	$$⊢\phi \to {opp}_{𝑔}\left(G\right)\in \mathrm{Mnd}$$
38	1 3 11 37 6 19 7 8 2 9	gsumzmhm	$$⊢\phi \to {\sum }_{{opp}_{𝑔}\left(G\right)}\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$
39	35 38	eqtr3d	$$⊢\phi \to {\sum }_G\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$