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