Theorem gsumval

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumval.b	$$⊢B={\mathrm{Base}}_G$$
	gsumval.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumval.o	$$⊢O=\left\{s\in B|\forall t\in B\left(s\underset{\dot{}}{+}t=t\wedge t\underset{\dot{}}{+}s=t\right)\right\}$$
	gsumval.w	$$⊢\phi \to W=F^{-1}\left[\mathrm{V}\setminus O\right]$$
	gsumval.g	$$⊢\phi \to G\in V$$
	gsumval.a	$$⊢\phi \to A\in X$$
	gsumval.f	$$⊢\phi \to F:A⟶B$$
Assertion	gsumval	$$⊢\phi \to {\sum }_{G}F=if\left(\mathrm{ran}F\subseteq O,\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)$$

Proof

Step	Hyp	Ref	Expression
1		gsumval.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumval.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		gsumval.o	$$⊢O=\left\{s\in B|\forall t\in B\left(s\underset{\dot{}}{+}t=t\wedge t\underset{\dot{}}{+}s=t\right)\right\}$$
5		gsumval.w	$$⊢\phi \to W=F^{-1}\left[\mathrm{V}\setminus O\right]$$
6		gsumval.g	$$⊢\phi \to G\in V$$
7		gsumval.a	$$⊢\phi \to A\in X$$
8		gsumval.f	$$⊢\phi \to F:A⟶B$$
9	1	fvexi	$$⊢B\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to B\in \mathrm{V}$$
11		fex2	$$⊢\left(F:A⟶B\wedge A\in X\wedge B\in \mathrm{V}\right)\to F\in \mathrm{V}$$
12	8 7 10 11	syl3anc	$$⊢\phi \to F\in \mathrm{V}$$
13	8	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
14	1 2 3 4 5 6 12 13	gsumvalx	$$⊢\phi \to {\sum }_{G}F=if\left(\mathrm{ran}F\subseteq O,\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)$$