Theorem gsumsub

Description: The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsumsub.b	$$⊢B={\mathrm{Base}}_G$$
	gsumsub.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumsub.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	gsumsub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	gsumsub.a	$$⊢\phi \to A\in V$$
	gsumsub.f	$$⊢\phi \to F:A⟶B$$
	gsumsub.h	$$⊢\phi \to H:A⟶B$$
	gsumsub.fn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
	gsumsub.hn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(H\right)$$
Assertion	gsumsub	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumsub.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumsub.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumsub.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		gsumsub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		gsumsub.a	$$⊢\phi \to A\in V$$
6		gsumsub.f	$$⊢\phi \to F:A⟶B$$
7		gsumsub.h	$$⊢\phi \to H:A⟶B$$
8		gsumsub.fn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
9		gsumsub.hn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(H\right)$$
10		eqid	$$⊢{+}_G={+}_G$$
11		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
12	4 11	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
13		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
14		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
15	4 14	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
16	1 13 15	grpinvf1o	$$⊢\phi \to {inv}_g\left(G\right):B\underset{1-1\; onto}{⟶}B$$
17		f1of	$$⊢{inv}_g\left(G\right):B\underset{1-1\; onto}{⟶}B\to {inv}_g\left(G\right):B⟶B$$
18	16 17	syl	$$⊢\phi \to {inv}_g\left(G\right):B⟶B$$
19		fco	$$⊢\left({inv}_g\left(G\right):B⟶B\wedge H:A⟶B\right)\to \left({inv}_g\left(G\right)\circ H\right):A⟶B$$
20	18 7 19	syl2anc	$$⊢\phi \to \left({inv}_g\left(G\right)\circ H\right):A⟶B$$
21	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
23	1	fvexi	$$⊢B\in \mathrm{V}$$
24	23	a1i	$$⊢\phi \to B\in \mathrm{V}$$
25	2 13	grpinvid	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
26	15 25	syl	$$⊢\phi \to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
27	22 7 18 5 24 9 26	fsuppco2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left({inv}_g\left(G\right)\circ H\right)\right)$$
28	1 2 10 12 5 6 20 8 27	gsumadd	$$⊢\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)$$
29	1 2 13 4 5 7 9	gsuminv	$$⊢\phi \to {\sum }_G\left({inv}_g\left(G\right)\circ H\right)={inv}_g\left(G\right)\left({\sum }_{G}H\right)$$
30	29	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)$$
31	28 30	eqtrd	$$⊢\phi \to {\sum }_G\left(F{{+}_G}_f\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)$$
32	6	ffvelrnda	$$⊢\left(\phi \wedge k\in A\right)\to F\left(k\right)\in B$$
33	7	ffvelrnda	$$⊢\left(\phi \wedge k\in A\right)\to H\left(k\right)\in B$$
34	1 10 13 3	grpsubval	$$⊢\left(F\left(k\right)\in B\wedge H\left(k\right)\in B\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)$$
35	32 33 34	syl2anc	$$⊢\left(\phi \wedge k\in A\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)$$
36	35	mpteq2dva	$$⊢\phi \to \left(k\in A⟼F\left(k\right)\underset{\dot{}}{-}H\left(k\right)\right)=\left(k\in A⟼F\left(k\right){+}_G{inv}_g\left(G\right)\left(H\left(k\right)\right)\right)$$
37	6	feqmptd	$$⊢\phi \to F=\left(k\in A⟼F\left(k\right)\right)$$
38	7	feqmptd	$$⊢\phi \to H=\left(k\in A⟼H\left(k\right)\right)$$
39	5 32 33 37 38	offval2	$$⊢\phi \to F{\underset{\dot{}}{-}}_{f}H=\left(k\in A⟼F\left(k\right)\underset{\dot{}}{-}H\left(k\right)\right)$$
40		fvexd	$$⊢\left(\phi \wedge k\in A\right)\to {inv}_g\left(G\right)\left(H\left(k\right)\right)\in \mathrm{V}$$
41	18	feqmptd	$$⊢\phi \to {inv}_g\left(G\right)=\left(x\in B⟼{inv}_g\left(G\right)\left(x\right)\right)$$
42		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)$$
43	33 38 41 42	fmptco	$$⊢\phi \to {inv}_g\left(G\right)\circ H=\left(k\in A⟼{inv}_g\left(G\right)\left(H\left(k\right)\right)\right)$$
44	5 32 40 37 43	offval2	$$⊢\phi \to F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)=\left(k\in A⟼F\left(k\right){+}_G{inv}_g\left(G\right)\left(H\left(k\right)\right)\right)$$
45	36 39 44	3eqtr4d	$$⊢\phi \to F{\underset{\dot{}}{-}}_{f}H=F{{+}_G}_f\left({inv}_g\left(G\right)\circ H\right)$$
46	45	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)$$
47	1 2 12 5 6 8	gsumcl	$$⊢\phi \to {\sum }_{G}F\in B$$
48	1 2 12 5 7 9	gsumcl	$$⊢\phi \to {\sum }_{G}H\in B$$
49	1 10 13 3	grpsubval	$$⊢\left({\sum }_{G}F\in B\wedge {\sum }_{G}H\in B\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)$$
50	47 48 49	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)$$
51	31 46 50	3eqtr4d	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$