Theorem gsumzres

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)

	Ref	Expression
Hypotheses	gsumzcl.b	$$⊢B={\mathrm{Base}}_G$$
	gsumzcl.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumzcl.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzcl.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumzcl.a	$$⊢\phi \to A\in V$$
	gsumzcl.f	$$⊢\phi \to F:A⟶B$$
	gsumzcl.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumzres.s	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq W$$
	gsumzres.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumzres	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F$$

Proof

Step	Hyp	Ref	Expression
1		gsumzcl.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumzcl.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumzcl.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
4		gsumzcl.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
5		gsumzcl.a	$$⊢\phi \to A\in V$$
6		gsumzcl.f	$$⊢\phi \to F:A⟶B$$
7		gsumzcl.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
8		gsumzres.s	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq W$$
9		gsumzres.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
10		inex1g	$$⊢A\in V\to A\cap W\in \mathrm{V}$$
11	5 10	syl	$$⊢\phi \to A\cap W\in \mathrm{V}$$
12	2	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\cap W\in \mathrm{V}\right)\to \underset{k\in A\cap W}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
13	4 11 12	syl2anc	$$⊢\phi \to \underset{k\in A\cap W}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
14	2	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
15	4 5 14	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	13 15	eqtr4d	$$⊢\phi \to \underset{k\in A\cap W}{{\sum }_G}\underset{\dot{}}{0}=\underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}$$
17	16	adantr	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to \underset{k\in A\cap W}{{\sum }_G}\underset{\dot{}}{0}=\underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}$$
18		resres	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_W={F\upharpoonright }_{\left(A\cap W\right)}$$
19		ffn	$$⊢F:A⟶B\to FFnA$$
20		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
21	6 19 20	3syl	$$⊢\phi \to {F\upharpoonright }_A=F$$
22	21	reseq1d	$$⊢\phi \to {\left({F\upharpoonright }_A\right)\upharpoonright }_W={F\upharpoonright }_W$$
23	18 22	eqtr3id	$$⊢\phi \to {F\upharpoonright }_{\left(A\cap W\right)}={F\upharpoonright }_W$$
24	23	adantr	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {F\upharpoonright }_{\left(A\cap W\right)}={F\upharpoonright }_W$$
25	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
26	25	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
27		ssid	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
28	27	a1i	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
29	6 5 26 28	gsumcllem	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to F=\left(k\in A⟼\underset{\dot{}}{0}\right)$$
30	29	reseq1d	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {F\upharpoonright }_{\left(A\cap W\right)}={\left(k\in A⟼\underset{\dot{}}{0}\right)\upharpoonright }_{\left(A\cap W\right)}$$
31		inss1	$$⊢A\cap W\subseteq A$$
32		resmpt	$$⊢A\cap W\subseteq A\to {\left(k\in A⟼\underset{\dot{}}{0}\right)\upharpoonright }_{\left(A\cap W\right)}=\left(k\in \left(A\cap W\right)⟼\underset{\dot{}}{0}\right)$$
33	31 32	ax-mp	$$⊢{\left(k\in A⟼\underset{\dot{}}{0}\right)\upharpoonright }_{\left(A\cap W\right)}=\left(k\in \left(A\cap W\right)⟼\underset{\dot{}}{0}\right)$$
34	30 33	eqtrdi	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {F\upharpoonright }_{\left(A\cap W\right)}=\left(k\in \left(A\cap W\right)⟼\underset{\dot{}}{0}\right)$$
35	24 34	eqtr3d	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {F\upharpoonright }_W=\left(k\in \left(A\cap W\right)⟼\underset{\dot{}}{0}\right)$$
36	35	oveq2d	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {\sum }_G\left({F\upharpoonright }_W\right)=\underset{k\in A\cap W}{{\sum }_G}\underset{\dot{}}{0}$$
37	29	oveq2d	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {\sum }_{G}F=\underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}$$
38	17 36 37	3eqtr4d	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F$$
39	38	ex	$$⊢\phi \to \left(F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F\right)$$
40		f1ofo	$$⊢f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}$$
41		forn	$$⊢f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to \mathrm{ran}f=F\mathrm{supp}\underset{\dot{}}{0}$$
42	40 41	syl	$$⊢f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to \mathrm{ran}f=F\mathrm{supp}\underset{\dot{}}{0}$$
43	42	ad2antll	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \mathrm{ran}f=F\mathrm{supp}\underset{\dot{}}{0}$$
44	8	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq W$$
45	43 44	eqsstrd	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \mathrm{ran}f\subseteq W$$
46		cores	$$⊢\mathrm{ran}f\subseteq W\to \left({F\upharpoonright }_W\right)\circ f=F\circ f$$
47	45 46	syl	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \left({F\upharpoonright }_W\right)\circ f=F\circ f$$
48	47	seqeq3d	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to seq1\left({+}_G,\left(\left({F\upharpoonright }_W\right)\circ f\right)\right)=seq1\left({+}_G,\left(F\circ f\right)\right)$$
49	48	fveq1d	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to seq1\left({+}_G,\left(\left({F\upharpoonright }_W\right)\circ f\right)\right)\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)=seq1\left({+}_G,\left(F\circ f\right)\right)\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)$$
50		eqid	$$⊢{+}_G={+}_G$$
51	4	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to G\in \mathrm{Mnd}$$
52	11	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to A\cap W\in \mathrm{V}$$
53	6	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to F:A⟶B$$
54		fssres	$$⊢\left(F:A⟶B\wedge A\cap W\subseteq A\right)\to \left({F\upharpoonright }_{\left(A\cap W\right)}\right):A\cap W⟶B$$
55	53 31 54	sylancl	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \left({F\upharpoonright }_{\left(A\cap W\right)}\right):A\cap W⟶B$$
56	23	feq1d	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left(A\cap W\right)}\right):A\cap W⟶B\leftrightarrow \left({F\upharpoonright }_W\right):A\cap W⟶B\right)$$
57	56	biimpa	$$⊢\left(\phi \wedge \left({F\upharpoonright }_{\left(A\cap W\right)}\right):A\cap W⟶B\right)\to \left({F\upharpoonright }_W\right):A\cap W⟶B$$
58	55 57	syldan	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \left({F\upharpoonright }_W\right):A\cap W⟶B$$
59		resss	$$⊢{F\upharpoonright }_W\subseteq F$$
60	59	rnssi	$$⊢\mathrm{ran}\left({F\upharpoonright }_W\right)\subseteq \mathrm{ran}F$$
61	3	cntzidss	$$⊢\left(\mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)\wedge \mathrm{ran}\left({F\upharpoonright }_W\right)\subseteq \mathrm{ran}F\right)\to \mathrm{ran}\left({F\upharpoonright }_W\right)\subseteq Z\left(\mathrm{ran}\left({F\upharpoonright }_W\right)\right)$$
62	7 60 61	sylancl	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_W\right)\subseteq Z\left(\mathrm{ran}\left({F\upharpoonright }_W\right)\right)$$
63	62	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \mathrm{ran}\left({F\upharpoonright }_W\right)\subseteq Z\left(\mathrm{ran}\left({F\upharpoonright }_W\right)\right)$$
64		simprl	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}$$
65		f1of1	$$⊢f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}F\mathrm{supp}\underset{\dot{}}{0}$$
66	65	ad2antll	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}F\mathrm{supp}\underset{\dot{}}{0}$$
67		suppssdm	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}F$$
68	67 6	fssdm	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq A$$
69	68 8	ssind	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq A\cap W$$
70	69	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq A\cap W$$
71		f1ss	$$⊢\left(f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\wedge F\mathrm{supp}\underset{\dot{}}{0}\subseteq A\cap W\right)\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}A\cap W$$
72	66 70 71	syl2anc	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}A\cap W$$
73	6 5	fexd	$$⊢\phi \to F\in \mathrm{V}$$
74		ressuppss	$$⊢\left(F\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
75	73 25 74	sylancl	$$⊢\phi \to \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
76		sseq2	$$⊢\mathrm{ran}f=F\mathrm{supp}\underset{\dot{}}{0}\to \left(\left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f\leftrightarrow \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}\right)$$
77	75 76	imbitrrid	$$⊢\mathrm{ran}f=F\mathrm{supp}\underset{\dot{}}{0}\to \left(\phi \to \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f\right)$$
78	40 41 77	3syl	$$⊢f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to \left(\phi \to \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f\right)$$
79	78	adantl	$$⊢\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\to \left(\phi \to \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f\right)$$
80	79	impcom	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \left({F\upharpoonright }_W\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f$$
81		eqid	$$⊢\left(\left({F\upharpoonright }_W\right)\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(\left({F\upharpoonright }_W\right)\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
82	1 2 50 3 51 52 58 63 64 72 80 81	gsumval3	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to {\sum }_G\left({F\upharpoonright }_W\right)=seq1\left({+}_G,\left(\left({F\upharpoonright }_W\right)\circ f\right)\right)\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)$$
83	5	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to A\in V$$
84	7	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
85	68	adantr	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq A$$
86		f1ss	$$⊢\left(f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\wedge F\mathrm{supp}\underset{\dot{}}{0}\subseteq A\right)\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}A$$
87	66 85 86	syl2anc	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}A$$
88	27 43	sseqtrrid	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f$$
89		eqid	$$⊢\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
90	1 2 50 3 51 83 53 84 64 87 88 89	gsumval3	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to {\sum }_{G}F=seq1\left({+}_G,\left(F\circ f\right)\right)\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)$$
91	49 82 90	3eqtr4d	$$⊢\left(\phi \wedge \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F$$
92	91	expr	$$⊢\left(\phi \wedge \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\right)\to \left(f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F\right)$$
93	92	exlimdv	$$⊢\left(\phi \wedge \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\right)\to \left(\exists ff:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F\right)$$
94	93	expimpd	$$⊢\phi \to \left(\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F\right)$$
95		fsuppimp	$$⊢{finSupp}_{\underset{\dot{}}{0}}\left(F\right)\to \left(\mathrm{Fun}F\wedge F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)$$
96	95	simprd	$$⊢{finSupp}_{\underset{\dot{}}{0}}\left(F\right)\to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
97		fz1f1o	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\to \left(F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \vee \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)$$
98	9 96 97	3syl	$$⊢\phi \to \left(F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \vee \left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1\; onto}{⟶}F\mathrm{supp}\underset{\dot{}}{0}\right)\right)$$
99	39 94 98	mpjaod	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F$$