Metamath Proof Explorer

Theorem gsumval

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumval.b 
|- B = ( Base ` G )
gsumval.z 
|- .0. = ( 0g ` G )
gsumval.p 
|- .+ = ( +g ` G )
gsumval.o 
|- O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }
gsumval.w 
|- ( ph -> W = ( `' F " ( _V \ O ) ) )
gsumval.g 
|- ( ph -> G e. V )
gsumval.a 
|- ( ph -> A e. X )
gsumval.f 
|- ( ph -> F : A --> B )
Assertion gsumval 
|- ( ph -> ( G gsum F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumval.b 
 |-  B = ( Base ` G )
2 gsumval.z 
 |-  .0. = ( 0g ` G )
3 gsumval.p 
 |-  .+ = ( +g ` G )
4 gsumval.o 
 |-  O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }
5 gsumval.w 
 |-  ( ph -> W = ( `' F " ( _V \ O ) ) )
6 gsumval.g 
 |-  ( ph -> G e. V )
7 gsumval.a 
 |-  ( ph -> A e. X )
8 gsumval.f 
 |-  ( ph -> F : A --> B )
9 1 fvexi 
 |-  B e. _V
10 9 a1i 
 |-  ( ph -> B e. _V )
11 fex2 
 |-  ( ( F : A --> B /\ A e. X /\ B e. _V ) -> F e. _V )
12 8 7 10 11 syl3anc 
 |-  ( ph -> F e. _V )
13 8 fdmd 
 |-  ( ph -> dom F = A )
14 1 2 3 4 5 6 12 13 gsumvalx 
 |-  ( ph -> ( G gsum F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )