Theorem dprdfsub

Description: Take the difference of group sums over two families 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$$
	dprdfadd.4	$$⊢\phi \to H\in W$$
	dprdfsub.b	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	dprdfsub	$$⊢\phi \to \left(F{\underset{\dot{}}{-}}_{f}H\in W\wedge {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\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		dprdfadd.4	$$⊢\phi \to H\in W$$
7		dprdfsub.b	$$⊢\underset{\dot{}}{-}={-}_G$$
8		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
9	2 3 4 5 8	dprdff	$$⊢\phi \to F:I⟶{\mathrm{Base}}_G$$
10	9	ffvelrnda	$$⊢\left(\phi \wedge k\in I\right)\to F\left(k\right)\in {\mathrm{Base}}_G$$
11	2 3 4 6 8	dprdff	$$⊢\phi \to H:I⟶{\mathrm{Base}}_G$$
12	11	ffvelrnda	$$⊢\left(\phi \wedge k\in I\right)\to H\left(k\right)\in {\mathrm{Base}}_G$$
13		eqid	$$⊢{+}_G={+}_G$$
14		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
15	8 13 14 7	grpsubval	$$⊢\left(F\left(k\right)\in {\mathrm{Base}}_G\wedge H\left(k\right)\in {\mathrm{Base}}_G\right)\to F\left(k\right)\underset{\dot{}}{-}H\left(k\right)=F\left(k\right){+}_G{inv}_g\left(G\right)\left(H\left(k\right)\right)$$
16	10 12 15	syl2anc	$$⊢\left(\phi \wedge k\in I\right)\to F\left(k\right)\underset{\dot{}}{-}H\left(k\right)=F\left(k\right){+}_G{inv}_g\left(G\right)\left(H\left(k\right)\right)$$
17	16	mpteq2dva	$$⊢\phi \to \left(k\in I⟼F\left(k\right)\underset{\dot{}}{-}H\left(k\right)\right)=\left(k\in I⟼F\left(k\right){+}_G{inv}_g\left(G\right)\left(H\left(k\right)\right)\right)$$
18	3 4	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
19	9	feqmptd	$$⊢\phi \to F=\left(k\in I⟼F\left(k\right)\right)$$
20	11	feqmptd	$$⊢\phi \to H=\left(k\in I⟼H\left(k\right)\right)$$
21	18 10 12 19 20	offval2	$$⊢\phi \to F{\underset{\dot{}}{-}}_{f}H=\left(k\in I⟼F\left(k\right)\underset{\dot{}}{-}H\left(k\right)\right)$$
22		fvexd	$$⊢\left(\phi \wedge k\in I\right)\to {inv}_g\left(G\right)\left(H\left(k\right)\right)\in \mathrm{V}$$
23		dprdgrp	$$⊢G\mathrm{dom}\mathrm{DProd}S\to G\in \mathrm{Grp}$$
24	3 23	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
25	8 14 24	grpinvf1o	$$⊢\phi \to {inv}_g\left(G\right):{\mathrm{Base}}_G\underset{1-1\; onto}{⟶}{\mathrm{Base}}_G$$
26		f1of	$$⊢{inv}_g\left(G\right):{\mathrm{Base}}_G\underset{1-1\; onto}{⟶}{\mathrm{Base}}_G\to {inv}_g\left(G\right):{\mathrm{Base}}_G⟶{\mathrm{Base}}_G$$
27	25 26	syl	$$⊢\phi \to {inv}_g\left(G\right):{\mathrm{Base}}_G⟶{\mathrm{Base}}_G$$
28	27	feqmptd	$$⊢\phi \to {inv}_g\left(G\right)=\left(x\in {\mathrm{Base}}_G⟼{inv}_g\left(G\right)\left(x\right)\right)$$
29		fveq2	$$⊢x=H\left(k\right)\to {inv}_g\left(G\right)\left(x\right)={inv}_g\left(G\right)\left(H\left(k\right)\right)$$
30	12 20 28 29	fmptco	$$⊢\phi \to {inv}_g\left(G\right)\circ H=\left(k\in I⟼{inv}_g\left(G\right)\left(H\left(k\right)\right)\right)$$
31	18 10 22 19 30	offval2	$$⊢\phi \to F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)=\left(k\in I⟼F\left(k\right){+}_G{inv}_g\left(G\right)\left(H\left(k\right)\right)\right)$$
32	17 21 31	3eqtr4d	$$⊢\phi \to F{\underset{\dot{}}{-}}_{f}H=F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)$$
33	1 2 3 4 6 14	dprdfinv	$$⊢\phi \to \left({inv}_g\left(G\right)\circ H\in W\wedge {\sum }_G\left({inv}_g\left(G\right)\circ H\right)={inv}_g\left(G\right)\left({\sum }_{G}H\right)\right)$$
34	33	simpld	$$⊢\phi \to {inv}_g\left(G\right)\circ H\in W$$
35	1 2 3 4 5 34 13	dprdfadd	$$⊢\phi \to \left(F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)\in W\wedge {\sum }_G\left(F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)\right)=\left({\sum }_G,F\right){+}_G\left({\sum }_G,\left({inv}_g\left(G\right)\circ H\right)\right)\right)$$
36	35	simpld	$$⊢\phi \to F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)\in W$$
37	32 36	eqeltrd	$$⊢\phi \to F{\underset{\dot{}}{-}}_{f}H\in W$$
38	32	oveq2d	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)={\sum }_G\left(F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)\right)$$
39	33	simprd	$$⊢\phi \to {\sum }_G\left({inv}_g\left(G\right)\circ H\right)={inv}_g\left(G\right)\left({\sum }_{G}H\right)$$
40	39	oveq2d	$$⊢\phi \to \left({\sum }_G,F\right){+}_G\left({\sum }_G,\left({inv}_g\left(G\right)\circ H\right)\right)=\left({\sum }_G,F\right){+}_G{inv}_g\left(G\right)\left({\sum }_{G}H\right)$$
41	35	simprd	$$⊢\phi \to {\sum }_G\left(F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)\right)=\left({\sum }_G,F\right){+}_G\left({\sum }_G,\left({inv}_g\left(G\right)\circ H\right)\right)$$
42	8	dprdssv	$$⊢G\mathrm{DProd}S\subseteq {\mathrm{Base}}_G$$
43	1 2 3 4 5	eldprdi	$$⊢\phi \to {\sum }_{G}F\in \left(G\mathrm{DProd}S\right)$$
44	42 43	sseldi	$$⊢\phi \to {\sum }_{G}F\in {\mathrm{Base}}_G$$
45	1 2 3 4 6	eldprdi	$$⊢\phi \to {\sum }_{G}H\in \left(G\mathrm{DProd}S\right)$$
46	42 45	sseldi	$$⊢\phi \to {\sum }_{G}H\in {\mathrm{Base}}_G$$
47	8 13 14 7	grpsubval	$$⊢\left({\sum }_{G}F\in {\mathrm{Base}}_G\wedge {\sum }_{G}H\in {\mathrm{Base}}_G\right)\to \left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)=\left({\sum }_G,F\right){+}_G{inv}_g\left(G\right)\left({\sum }_{G}H\right)$$
48	44 46 47	syl2anc	$$⊢\phi \to \left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)=\left({\sum }_G,F\right){+}_G{inv}_g\left(G\right)\left({\sum }_{G}H\right)$$
49	40 41 48	3eqtr4d	$$⊢\phi \to {\sum }_G\left(F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$
50	38 49	eqtrd	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$
51	37 50	jca	$$⊢\phi \to \left(F{\underset{\dot{}}{-}}_{f}H\in W\wedge {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)\right)$$