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

Metamath Proof Explorer

Theorem gsum0

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

Ref Expression
Hypothesis gsum0.z 
|- .0. = ( 0g ` G )
Assertion gsum0 
|- ( G gsum (/) ) = .0.

Proof

Step Hyp Ref Expression
1 gsum0.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 id 
 |-  ( G e. _V -> G e. _V )
6 0ex 
 |-  (/) e. _V
7 6 a1i 
 |-  ( G e. _V -> (/) e. _V )
8 f0 
 |-  (/) : (/) --> { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) }
9 8 a1i 
 |-  ( G e. _V -> (/) : (/) --> { x e. ( Base ` G ) | A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) = y /\ ( y ( +g ` G ) x ) = y ) } )
10 2 1 3 4 5 7 9 gsumval1 
 |-  ( G e. _V -> ( G gsum (/) ) = .0. )
11 df-gsum 
 |-  gsum = ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) ) )
12 11 reldmmpo 
 |-  Rel dom gsum
13 12 ovprc1 
 |-  ( -. G e. _V -> ( G gsum (/) ) = (/) )
14 fvprc 
 |-  ( -. G e. _V -> ( 0g ` G ) = (/) )
15 1 14 eqtrid 
 |-  ( -. G e. _V -> .0. = (/) )
16 13 15 eqtr4d 
 |-  ( -. G e. _V -> ( G gsum (/) ) = .0. )
17 10 16 pm2.61i 
 |-  ( G gsum (/) ) = .0.