Theorem dprdfinv

Description: Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
	eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
	eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
	eldprdi.3	$$⊢\phi \to F\in W$$
	dprdfinv.b	$$⊢N={inv}_g\left(G\right)$$
Assertion	dprdfinv	$$⊢\phi \to \left(N\circ F\in W\wedge {\sum }_G\left(N\circ F\right)=N\left({\sum }_{G}F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
3		eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
4		eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
5		eldprdi.3	$$⊢\phi \to F\in W$$
6		dprdfinv.b	$$⊢N={inv}_g\left(G\right)$$
7		dprdgrp	$$⊢G\mathrm{dom}\mathrm{DProd}S\to G\in \mathrm{Grp}$$
8	3 7	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
9		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
10	9 6	grpinvf	$$⊢G\in \mathrm{Grp}\to N:{\mathrm{Base}}_G⟶{\mathrm{Base}}_G$$
11	8 10	syl	$$⊢\phi \to N:{\mathrm{Base}}_G⟶{\mathrm{Base}}_G$$
12	2 3 4 5 9	dprdff	$$⊢\phi \to F:I⟶{\mathrm{Base}}_G$$
13		fcompt	$$⊢\left(N:{\mathrm{Base}}_G⟶{\mathrm{Base}}_G\wedge F:I⟶{\mathrm{Base}}_G\right)\to N\circ F=\left(x\in I⟼N\left(F\left(x\right)\right)\right)$$
14	11 12 13	syl2anc	$$⊢\phi \to N\circ F=\left(x\in I⟼N\left(F\left(x\right)\right)\right)$$
15	3 4	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
16	15	ffvelrnda	$$⊢\left(\phi \wedge x\in I\right)\to S\left(x\right)\in \mathrm{SubGrp}\left(G\right)$$
17	2 3 4 5	dprdfcl	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)\in S\left(x\right)$$
18	6	subginvcl	$$⊢\left(S\left(x\right)\in \mathrm{SubGrp}\left(G\right)\wedge F\left(x\right)\in S\left(x\right)\right)\to N\left(F\left(x\right)\right)\in S\left(x\right)$$
19	16 17 18	syl2anc	$$⊢\left(\phi \wedge x\in I\right)\to N\left(F\left(x\right)\right)\in S\left(x\right)$$
20	3 4	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
21	20	mptexd	$$⊢\phi \to \left(x\in I⟼N\left(F\left(x\right)\right)\right)\in \mathrm{V}$$
22		funmpt	$$⊢\mathrm{Fun}\left(x\in I⟼N\left(F\left(x\right)\right)\right)$$
23	22	a1i	$$⊢\phi \to \mathrm{Fun}\left(x\in I⟼N\left(F\left(x\right)\right)\right)$$
24	2 3 4 5	dprdffsupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
25		ssidd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
26	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
27	26	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
28	12 25 20 27	suppssr	$$⊢\left(\phi \wedge x\in \left(I\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to F\left(x\right)=\underset{\dot{}}{0}$$
29	28	fveq2d	$$⊢\left(\phi \wedge x\in \left(I\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to N\left(F\left(x\right)\right)=N\left(\underset{\dot{}}{0}\right)$$
30	1 6	grpinvid	$$⊢G\in \mathrm{Grp}\to N\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
31	8 30	syl	$$⊢\phi \to N\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
32	31	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to N\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
33	29 32	eqtrd	$$⊢\left(\phi \wedge x\in \left(I\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to N\left(F\left(x\right)\right)=\underset{\dot{}}{0}$$
34	33 20	suppss2	$$⊢\phi \to \left(x\in I⟼N\left(F\left(x\right)\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
35		fsuppsssupp	$$⊢\left(\left(\left(x\in I⟼N\left(F\left(x\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(x\in I⟼N\left(F\left(x\right)\right)\right)\right)\wedge \left({finSupp}_{\underset{\dot{}}{0}}\left(F\right)\wedge \left(x\in I⟼N\left(F\left(x\right)\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in I⟼N\left(F\left(x\right)\right)\right)\right)$$
36	21 23 24 34 35	syl22anc	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in I⟼N\left(F\left(x\right)\right)\right)\right)$$
37	2 3 4 19 36	dprdwd	$$⊢\phi \to \left(x\in I⟼N\left(F\left(x\right)\right)\right)\in W$$
38	14 37	eqeltrd	$$⊢\phi \to N\circ F\in W$$
39		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
40	2 3 4 5 39	dprdfcntz	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}F\right)$$
41	9 1 39 6 8 20 12 40 24	gsumzinv	$$⊢\phi \to {\sum }_G\left(N\circ F\right)=N\left({\sum }_{G}F\right)$$
42	38 41	jca	$$⊢\phi \to \left(N\circ F\in W\wedge {\sum }_G\left(N\circ F\right)=N\left({\sum }_{G}F\right)\right)$$