Theorem gsumz

Description: Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypothesis	gsumz.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		gsumz.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		simpl	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to G\in \mathrm{Mnd}$$
6		simpr	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to A\in V$$
7	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
8	7	snid	$$⊢\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
9	2 1 3 4	gsumvallem2	$$⊢G\in \mathrm{Mnd}\to \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\{\underset{\dot{}}{0}\right\}$$
10	8 9	eleqtrrid	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in \left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}$$
11	10	ad2antrr	$$⊢\left(\left(G\in \mathrm{Mnd}\wedge A\in V\right)\wedge k\in A\right)\to \underset{\dot{}}{0}\in \left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}$$
12	11	fmpttd	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \left(k\in A⟼\underset{\dot{}}{0}\right):A⟶\left\{x\in {\mathrm{Base}}_G|\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y=y\wedge y{+}_{G}x=y\right)\right\}$$
13	2 1 3 4 5 6 12	gsumval1	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$