This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. )