Step |
Hyp |
Ref |
Expression |
1 |
|
gsumval3.b |
|- B = ( Base ` G ) |
2 |
|
gsumval3.0 |
|- .0. = ( 0g ` G ) |
3 |
|
gsumval3.p |
|- .+ = ( +g ` G ) |
4 |
|
gsumval3.z |
|- Z = ( Cntz ` G ) |
5 |
|
gsumval3.g |
|- ( ph -> G e. Mnd ) |
6 |
|
gsumval3.a |
|- ( ph -> A e. V ) |
7 |
|
gsumval3.f |
|- ( ph -> F : A --> B ) |
8 |
|
gsumval3.c |
|- ( ph -> ran F C_ ( Z ` ran F ) ) |
9 |
|
gsumval3a.t |
|- ( ph -> W e. Fin ) |
10 |
|
gsumval3a.n |
|- ( ph -> W =/= (/) ) |
11 |
|
gsumval3a.w |
|- W = ( F supp .0. ) |
12 |
|
gsumval3a.i |
|- ( ph -> -. A e. ran ... ) |
13 |
|
eqid |
|- { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } |
14 |
11
|
a1i |
|- ( ph -> W = ( F supp .0. ) ) |
15 |
7 6
|
fexd |
|- ( ph -> F e. _V ) |
16 |
2
|
fvexi |
|- .0. e. _V |
17 |
|
suppimacnv |
|- ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
18 |
15 16 17
|
sylancl |
|- ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
19 |
1 2 3 13
|
gsumvallem2 |
|- ( G e. Mnd -> { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { .0. } ) |
20 |
5 19
|
syl |
|- ( ph -> { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } = { .0. } ) |
21 |
20
|
eqcomd |
|- ( ph -> { .0. } = { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) |
22 |
21
|
difeq2d |
|- ( ph -> ( _V \ { .0. } ) = ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) |
23 |
22
|
imaeq2d |
|- ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( `' F " ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) ) |
24 |
14 18 23
|
3eqtrd |
|- ( ph -> W = ( `' F " ( _V \ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) ) |
25 |
1 2 3 13 24 5 6 7
|
gsumval |
|- ( ph -> ( G gsum F ) = if ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } , .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 ) ) ) ) ) ) ) |
26 |
20
|
sseq2d |
|- ( ph -> ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } <-> ran F C_ { .0. } ) ) |
27 |
11
|
a1i |
|- ( ( ph /\ ran F C_ { .0. } ) -> W = ( F supp .0. ) ) |
28 |
7 6
|
jca |
|- ( ph -> ( F : A --> B /\ A e. V ) ) |
29 |
28
|
adantr |
|- ( ( ph /\ ran F C_ { .0. } ) -> ( F : A --> B /\ A e. V ) ) |
30 |
|
fex |
|- ( ( F : A --> B /\ A e. V ) -> F e. _V ) |
31 |
29 30
|
syl |
|- ( ( ph /\ ran F C_ { .0. } ) -> F e. _V ) |
32 |
31 16 17
|
sylancl |
|- ( ( ph /\ ran F C_ { .0. } ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
33 |
7
|
ffnd |
|- ( ph -> F Fn A ) |
34 |
33
|
adantr |
|- ( ( ph /\ ran F C_ { .0. } ) -> F Fn A ) |
35 |
|
simpr |
|- ( ( ph /\ ran F C_ { .0. } ) -> ran F C_ { .0. } ) |
36 |
|
df-f |
|- ( F : A --> { .0. } <-> ( F Fn A /\ ran F C_ { .0. } ) ) |
37 |
34 35 36
|
sylanbrc |
|- ( ( ph /\ ran F C_ { .0. } ) -> F : A --> { .0. } ) |
38 |
|
disjdif |
|- ( { .0. } i^i ( _V \ { .0. } ) ) = (/) |
39 |
|
fimacnvdisj |
|- ( ( F : A --> { .0. } /\ ( { .0. } i^i ( _V \ { .0. } ) ) = (/) ) -> ( `' F " ( _V \ { .0. } ) ) = (/) ) |
40 |
37 38 39
|
sylancl |
|- ( ( ph /\ ran F C_ { .0. } ) -> ( `' F " ( _V \ { .0. } ) ) = (/) ) |
41 |
27 32 40
|
3eqtrd |
|- ( ( ph /\ ran F C_ { .0. } ) -> W = (/) ) |
42 |
41
|
ex |
|- ( ph -> ( ran F C_ { .0. } -> W = (/) ) ) |
43 |
26 42
|
sylbid |
|- ( ph -> ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } -> W = (/) ) ) |
44 |
43
|
necon3ad |
|- ( ph -> ( W =/= (/) -> -. ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) ) |
45 |
10 44
|
mpd |
|- ( ph -> -. ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } ) |
46 |
45
|
iffalsed |
|- ( ph -> if ( ran F C_ { z e. B | A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) } , .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 ) ) ) ) ) ) = 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 ) ) ) ) ) ) |
47 |
12
|
iffalsed |
|- ( ph -> 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 ) ) ) ) ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |
48 |
25 46 47
|
3eqtrd |
|- ( ph -> ( G gsum F ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |