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		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
12	5 11	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
13	1 4	grpinvf	$$⊢G\in \mathrm{Grp}\to I:B⟶B$$
14	5 13	syl	$$⊢\phi \to I:B⟶B$$
15		fco	$$⊢\left(I:B⟶B\wedge F:A⟶B\right)\to \left(I\circ F\right):A⟶B$$
16	14 7 15	syl2anc	$$⊢\phi \to \left(I\circ F\right):A⟶B$$
17	10 4	invoppggim	$$⊢G\in \mathrm{Grp}\to I\in \left(G\mathrm{GrpIso}{opp}_{𝑔}\left(G\right)\right)$$
18		gimghm	$$⊢I\in \left(G\mathrm{GrpIso}{opp}_{𝑔}\left(G\right)\right)\to I\in \left(G\mathrm{GrpHom}{opp}_{𝑔}\left(G\right)\right)$$
19		ghmmhm	$$⊢I\in \left(G\mathrm{GrpHom}{opp}_{𝑔}\left(G\right)\right)\to I\in \left(G\mathrm{MndHom}{opp}_{𝑔}\left(G\right)\right)$$
20	5 17 18 19	4syl	$$⊢\phi \to I\in \left(G\mathrm{MndHom}{opp}_{𝑔}\left(G\right)\right)$$
21		eqid	$$⊢\mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)=\mathrm{Cntz}\left({opp}_{𝑔}\left(G\right)\right)$$
22	3 21	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)$$
23	20 8 22	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)$$
24		rnco2	$$⊢\mathrm{ran}\left(I\circ F\right)=I\left[\mathrm{ran}F\right]$$
25	24	fveq2i	$$⊢Z\left(\mathrm{ran}\left(I\circ F\right)\right)=Z\left(I\left[\mathrm{ran}F\right]\right)$$
26	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)$$
27	25 26	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)$$
28	23 24 27	3sstr4g	$$⊢\phi \to \mathrm{ran}\left(I\circ F\right)\subseteq Z\left(\mathrm{ran}\left(I\circ F\right)\right)$$
29	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
30	29	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
31	1	fvexi	$$⊢B\in \mathrm{V}$$
32	31	a1i	$$⊢\phi \to B\in \mathrm{V}$$
33	2 4	grpinvid	$$⊢G\in \mathrm{Grp}\to I\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
34	5 33	syl	$$⊢\phi \to I\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
35	30 7 14 6 32 9 34	fsuppco2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(I\circ F\right)\right)$$
36	1 2 3 10 12 6 16 28 35	gsumzoppg	$$⊢\phi \to {\sum }_{{opp}_{𝑔}\left(G\right)}\left(I\circ F\right)={\sum }_G\left(I\circ F\right)$$
37	10	oppgmnd	$$⊢G\in \mathrm{Mnd}\to {opp}_{𝑔}\left(G\right)\in \mathrm{Mnd}$$
38	12 37	syl	$$⊢\phi \to {opp}_{𝑔}\left(G\right)\in \mathrm{Mnd}$$
39	1 3 12 38 6 20 7 8 2 9	gsumzmhm	$$⊢\phi \to {\sum }_{{opp}_{𝑔}\left(G\right)}\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$
40	36 39	eqtr3d	$$⊢\phi \to {\sum }_G\left(I\circ F\right)=I\left({\sum }_{G}F\right)$$