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