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	syl5eq	|- ( -. G e. _V -> .0. = (/) )
16	13 15	eqtr4d	|- ( -. G e. _V -> ( G gsum (/) ) = .0. )
17	10 16	pm2.61i	|- ( G gsum (/) ) = .0.