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

Metamath Proof Explorer

Theorem gsumval1

Description: Value of the group sum operation when every element being summed is an identity of G . (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumval1.b 
|- B = ( Base ` G )
gsumval1.z 
|- .0. = ( 0g ` G )
gsumval1.p 
|- .+ = ( +g ` G )
gsumval1.o 
|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
gsumval1.g 
|- ( ph -> G e. V )
gsumval1.a 
|- ( ph -> A e. W )
gsumval1.f 
|- ( ph -> F : A --> O )
Assertion gsumval1 
|- ( ph -> ( G gsum F ) = .0. )

Proof

Step Hyp Ref Expression
1 gsumval1.b 
 |-  B = ( Base ` G )
2 gsumval1.z 
 |-  .0. = ( 0g ` G )
3 gsumval1.p 
 |-  .+ = ( +g ` G )
4 gsumval1.o 
 |-  O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
5 gsumval1.g 
 |-  ( ph -> G e. V )
6 gsumval1.a 
 |-  ( ph -> A e. W )
7 gsumval1.f 
 |-  ( ph -> F : A --> O )
8 eqidd 
 |-  ( ph -> ( `' F " ( _V \ O ) ) = ( `' F " ( _V \ O ) ) )
9 4 ssrab3 
 |-  O C_ B
10 fss 
 |-  ( ( F : A --> O /\ O C_ B ) -> F : A --> B )
11 7 9 10 sylancl 
 |-  ( ph -> F : A --> B )
12 1 2 3 4 8 5 6 11 gsumval 
 |-  ( ph -> ( G gsum F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) ) )
13 frn 
 |-  ( F : A --> O -> ran F C_ O )
14 iftrue 
 |-  ( ran F C_ O -> if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) ) = .0. )
15 7 13 14 3syl 
 |-  ( ph -> if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ O ) ) ) ) -1-1-onto-> ( `' F " ( _V \ O ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ O ) ) ) ) ) ) ) ) = .0. )
16 12 15 eqtrd 
 |-  ( ph -> ( G gsum F ) = .0. )