Theorem gsumz

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

	Ref	Expression
Hypothesis	gsumz.z	|- .0. = ( 0g ` G )
Assertion	gsumz	|- ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		gsumz.z	|- .0. = ( 0g ` G )
2		eqid	|- ( Base ` G ) = ( Base ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4		eqid	|- { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) } = { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) }
5		simpl	|- ( ( G e. Mnd /\ A e. V ) -> G e. Mnd )
6		simpr	|- ( ( G e. Mnd /\ A e. V ) -> A e. V )
7	1	fvexi	|- .0. e. _V
8	7	snid	|- .0. e. { .0. }
9	2 1 3 4	gsumvallem2	|- ( G e. Mnd -> { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) } = { .0. } )
10	8 9	eleqtrrid	|- ( G e. Mnd -> .0. e. { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) } )
11	10	ad2antrr	|- ( ( ( G e. Mnd /\ A e. V ) /\ k e. A ) -> .0. e. { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) } )
12	11	fmpttd	|- ( ( G e. Mnd /\ A e. V ) -> ( k e. A |-> .0. ) : A --> { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) } )
13	2 1 3 4 5 6 12	gsumval1	|- ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )