Theorem gsum0

Description: Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypothesis	gsum0.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	gsum0	$$⊢{\sum }_G\varnothing =\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		gsum0.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4		eqid	$$⊢\left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}=\left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}$$
5		id	$$⊢G\in \mathrm{V}\to G\in \mathrm{V}$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	6	a1i	$$⊢G\in \mathrm{V}\to \varnothing \in \mathrm{V}$$
8		f0	$$⊢\varnothing :\varnothing ⟶\left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}$$
9	8	a1i	$$⊢G\in \mathrm{V}\to \varnothing :\varnothing ⟶\left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}$$
10	2 1 3 4 5 7 9	gsumval1	$$⊢G\in \mathrm{V}\to {\sum }_G\varnothing =\underset{\dot{}}{0}$$
11		df-gsum	$$⊢{\Sigma }_{𝑔}=\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left\{x\in {\mathrm{Base}}_w|\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)\right\}/o⦌if\left(\mathrm{ran}f\subseteq o,0_w,if\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)\right)\right)$$
12	11	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\Sigma }_{𝑔}$$
13	12	ovprc1	$$⊢\neg G\in \mathrm{V}\to {\sum }_G\varnothing =\varnothing$$
14		fvprc	$$⊢\neg G\in \mathrm{V}\to 0_G=\varnothing$$
15	1 14	eqtrid	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{0}=\varnothing$$
16	13 15	eqtr4d	$$⊢\neg G\in \mathrm{V}\to {\sum }_G\varnothing =\underset{\dot{}}{0}$$
17	10 16	pm2.61i	$$⊢{\sum }_G\varnothing =\underset{\dot{}}{0}$$