gsumz

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

		Ref	Expression
	Hypothesis	gsumz.z	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	gsumz	$⊢ (G \in Mnd \land A \in V) \to \underset{k \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		gsumz.z	$⊢ \underset{˙}{0} = 0_{G}$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4		eqid	$⊢ \{x \in {Base}_{G} \| \forall y \in {Base}_{G} (x +_{G} y = y \land y +_{G} x = y)\} = \{x \in {Base}_{G} \| \forall y \in {Base}_{G} (x +_{G} y = y \land y +_{G} x = y)\}$
5		simpl	$⊢ (G \in Mnd \land A \in V) \to G \in Mnd$
6		simpr	$⊢ (G \in Mnd \land A \in V) \to A \in V$
7	1	fvexi	$⊢ \underset{˙}{0} \in V$
8	7	snid	$⊢ \underset{˙}{0} \in \{\underset{˙}{0}\}$
9	2 1 3 4	gsumvallem2	$⊢ G \in Mnd \to \{x \in {Base}_{G} \| \forall y \in {Base}_{G} (x +_{G} y = y \land y +_{G} x = y)\} = \{\underset{˙}{0}\}$
10	8 9	eleqtrrid	$⊢ G \in Mnd \to \underset{˙}{0} \in \{x \in {Base}_{G} \| \forall y \in {Base}_{G} (x +_{G} y = y \land y +_{G} x = y)\}$
11	10	ad2antrr	$⊢ ((G \in Mnd \land A \in V) \land k \in A) \to \underset{˙}{0} \in \{x \in {Base}_{G} \| \forall y \in {Base}_{G} (x +_{G} y = y \land y +_{G} x = y)\}$
12	11	fmpttd	$⊢ (G \in Mnd \land A \in V) \to (k \in A ⟼ \underset{˙}{0}) : A ⟶ \{x \in {Base}_{G} \| \forall y \in {Base}_{G} (x +_{G} y = y \land y +_{G} x = y)\}$
13	2 1 3 4 5 6 12	gsumval1	$⊢ (G \in Mnd \land A \in V) \to \underset{k \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer