Theorem gsumval3a

Description: Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014) (Revised by AV, 29-May-2019)

	Ref	Expression
Hypotheses	gsumval3.b	$$⊢B={\mathrm{Base}}_G$$
	gsumval3.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumval3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumval3.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumval3.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumval3.a	$$⊢\phi \to A\in V$$
	gsumval3.f	$$⊢\phi \to F:A⟶B$$
	gsumval3.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumval3a.t	$$⊢\phi \to W\in \mathrm{Fin}$$
	gsumval3a.n	$$⊢\phi \to W\ne \varnothing$$
	gsumval3a.w	$$⊢W=F\mathrm{supp}\underset{\dot{}}{0}$$
	gsumval3a.i	$$⊢\phi \to \neg A\in \mathrm{ran}\dots$$
Assertion	gsumval3a	$$⊢\phi \to {\sum }_{G}F=\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumval3.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumval3.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumval3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		gsumval3.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
5		gsumval3.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
6		gsumval3.a	$$⊢\phi \to A\in V$$
7		gsumval3.f	$$⊢\phi \to F:A⟶B$$
8		gsumval3.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
9		gsumval3a.t	$$⊢\phi \to W\in \mathrm{Fin}$$
10		gsumval3a.n	$$⊢\phi \to W\ne \varnothing$$
11		gsumval3a.w	$$⊢W=F\mathrm{supp}\underset{\dot{}}{0}$$
12		gsumval3a.i	$$⊢\phi \to \neg A\in \mathrm{ran}\dots$$
13		eqid	$$⊢\left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}=\left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}$$
14	11	a1i	$$⊢\phi \to W=F\mathrm{supp}\underset{\dot{}}{0}$$
15	7 6	fexd	$$⊢\phi \to F\in \mathrm{V}$$
16	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
17		suppimacnv	$$⊢\left(F\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
18	15 16 17	sylancl	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
19	1 2 3 13	gsumvallem2	$$⊢G\in \mathrm{Mnd}\to \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}=\left\{\underset{\dot{}}{0}\right\}$$
20	5 19	syl	$$⊢\phi \to \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}=\left\{\underset{\dot{}}{0}\right\}$$
21	20	eqcomd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}=\left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}$$
22	21	difeq2d	$$⊢\phi \to \mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{V}\setminus \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}$$
23	22	imaeq2d	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=F^{-1}\left[\mathrm{V}\setminus \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}\right]$$
24	14 18 23	3eqtrd	$$⊢\phi \to W=F^{-1}\left[\mathrm{V}\setminus \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}\right]$$
25	1 2 3 13 24 5 6 7	gsumval	$$⊢\phi \to {\sum }_{G}F=if\left(\mathrm{ran}F\subseteq \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\},\underset{\dot{}}{0},if\left(A\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge x=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)\right)\right)$$
26	20	sseq2d	$$⊢\phi \to \left(\mathrm{ran}F\subseteq \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}\leftrightarrow \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)$$
27	11	a1i	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to W=F\mathrm{supp}\underset{\dot{}}{0}$$
28	7 6	jca	$$⊢\phi \to \left(F:A⟶B\wedge A\in V\right)$$
29	28	adantr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to \left(F:A⟶B\wedge A\in V\right)$$
30		fex	$$⊢\left(F:A⟶B\wedge A\in V\right)\to F\in \mathrm{V}$$
31	29 30	syl	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to F\in \mathrm{V}$$
32	31 16 17	sylancl	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
33	7	ffnd	$$⊢\phi \to FFnA$$
34	33	adantr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to FFnA$$
35		simpr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}$$
36		df-f	$$⊢F:A⟶\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(FFnA\wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)$$
37	34 35 36	sylanbrc	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to F:A⟶\left\{\underset{\dot{}}{0}\right\}$$
38		disjdif	$$⊢\left\{\underset{\dot{}}{0}\right\}\cap \left(\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right)=\varnothing$$
39		fimacnvdisj	$$⊢\left(F:A⟶\left\{\underset{\dot{}}{0}\right\}\wedge \left\{\underset{\dot{}}{0}\right\}\cap \left(\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right)=\varnothing \right)\to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing$$
40	37 38 39	sylancl	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing$$
41	27 32 40	3eqtrd	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\right)\to W=\varnothing$$
42	41	ex	$$⊢\phi \to \left(\mathrm{ran}F\subseteq \left\{\underset{\dot{}}{0}\right\}\to W=\varnothing \right)$$
43	26 42	sylbid	$$⊢\phi \to \left(\mathrm{ran}F\subseteq \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}\to W=\varnothing \right)$$
44	43	necon3ad	$$⊢\phi \to \left(W\ne \varnothing \to \neg \mathrm{ran}F\subseteq \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}\right)$$
45	10 44	mpd	$$⊢\phi \to \neg \mathrm{ran}F\subseteq \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\}$$
46	45	iffalsed	$$⊢\phi \to if\left(\mathrm{ran}F\subseteq \left\{z\in B|\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\right\},\underset{\dot{}}{0},if\left(A\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge x=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)\right)\right)=if\left(A\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge x=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)\right)$$
47	12	iffalsed	$$⊢\phi \to if\left(A\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge x=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)\right)=\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)$$
48	25 46 47	3eqtrd	$$⊢\phi \to {\sum }_{G}F=\left(\iota x|\exists f\left(f:\left(1\dots \left|W\right|\right)\underset{1-1\; onto}{⟶}W\wedge x=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|W\right|\right)\right)\right)$$