Theorem gsumzcl2

Description: Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl , because it is not required that F is a function (actually, the hypothesis always holds for any proper class F ). (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-Jun-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)$$
	gsumzcl2.w	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
Assertion	gsumzcl2	$$⊢\phi \to {\sum }_{G}F\in B$$

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		gsumzcl2.w	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
9	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
11		ssidd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
12	6 5 10 11	gsumcllem	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to F=\left(k\in A⟼\underset{\dot{}}{0}\right)$$
13	12	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}$$
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	15	adantr	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
17	13 16	eqtrd	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {\sum }_{G}F=\underset{\dot{}}{0}$$
18	1 2	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
19	4 18	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
20	19	adantr	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to \underset{\dot{}}{0}\in B$$
21	17 20	eqeltrd	$$⊢\left(\phi \wedge F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \right)\to {\sum }_{G}F\in B$$
22	21	ex	$$⊢\phi \to \left(F\mathrm{supp}\underset{\dot{}}{0}=\varnothing \to {\sum }_{G}F\in B\right)$$
23		eqid	$$⊢{+}_G={+}_G$$
24	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}$$
25	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$$
26	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$$
27	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)$$
28		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}$$
29		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}$$
30	29	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}$$
31		suppssdm	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}F$$
32	31 6	fssdm	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq A$$
33	32	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$$
34		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$$
35	30 33 34	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$$
36		ssid	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
37		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}$$
38		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}$$
39	37 38	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}$$
40	39	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}$$
41	36 40	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$$
42		eqid	$$⊢\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
43	1 2 23 3 24 25 26 27 28 35 41 42	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)$$
44		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
45	28 44	eleqtrdi	$$⊢\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{Z}}_{\ge 1}$$
46		f1f	$$⊢f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\underset{1-1}{⟶}A\to f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)⟶A$$
47	35 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 f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)⟶A$$
48		fco	$$⊢\left(F:A⟶B\wedge f:\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)⟶A\right)\to \left(F\circ f\right):\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)⟶B$$
49	26 47 48	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 \left(F\circ f\right):\left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)⟶B$$
50	49	ffvelcdmda	$$⊢\left(\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)\wedge k\in \left(1\dots \left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\right)\to \left(F\circ f\right)\left(k\right)\in B$$
51	1 23	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge k\in B\wedge x\in B\right)\to k{+}_{G}x\in B$$
52	51	3expb	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(k\in B\wedge x\in B\right)\right)\to k{+}_{G}x\in B$$
53	24 52	sylan	$$⊢\left(\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)\wedge \left(k\in B\wedge x\in B\right)\right)\to k{+}_{G}x\in B$$
54	45 50 53	seqcl	$$⊢\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(F\circ f\right)\right)\left(\left|F\mathrm{supp}\underset{\dot{}}{0}\right|\right)\in B$$
55	43 54	eqeltrd	$$⊢\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\in B$$
56	55	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}F\in B\right)$$
57	56	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}F\in B\right)$$
58	57	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}F\in B\right)$$
59		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)$$
60	8 59	syl	$$⊢\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)$$
61	22 58 60	mpjaod	$$⊢\phi \to {\sum }_{G}F\in B$$