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