Step |
Hyp |
Ref |
Expression |
1 |
|
gsumpropd.f |
|- ( ph -> F e. V ) |
2 |
|
gsumpropd.g |
|- ( ph -> G e. W ) |
3 |
|
gsumpropd.h |
|- ( ph -> H e. X ) |
4 |
|
gsumpropd.b |
|- ( ph -> ( Base ` G ) = ( Base ` H ) ) |
5 |
|
gsumpropd.p |
|- ( ph -> ( +g ` G ) = ( +g ` H ) ) |
6 |
5
|
oveqd |
|- ( ph -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) ) |
7 |
6
|
eqeq1d |
|- ( ph -> ( ( s ( +g ` G ) t ) = t <-> ( s ( +g ` H ) t ) = t ) ) |
8 |
5
|
oveqd |
|- ( ph -> ( t ( +g ` G ) s ) = ( t ( +g ` H ) s ) ) |
9 |
8
|
eqeq1d |
|- ( ph -> ( ( t ( +g ` G ) s ) = t <-> ( t ( +g ` H ) s ) = t ) ) |
10 |
7 9
|
anbi12d |
|- ( ph -> ( ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) <-> ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) ) ) |
11 |
4 10
|
raleqbidv |
|- ( ph -> ( A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) <-> A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) ) ) |
12 |
4 11
|
rabeqbidv |
|- ( ph -> { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } = { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) |
13 |
12
|
sseq2d |
|- ( ph -> ( ran F C_ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } <-> ran F C_ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) |
14 |
|
eqidd |
|- ( ph -> ( Base ` G ) = ( Base ` G ) ) |
15 |
5
|
oveqdr |
|- ( ( ph /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) = ( a ( +g ` H ) b ) ) |
16 |
14 4 15
|
grpidpropd |
|- ( ph -> ( 0g ` G ) = ( 0g ` H ) ) |
17 |
5
|
seqeq2d |
|- ( ph -> seq m ( ( +g ` G ) , F ) = seq m ( ( +g ` H ) , F ) ) |
18 |
17
|
fveq1d |
|- ( ph -> ( seq m ( ( +g ` G ) , F ) ` n ) = ( seq m ( ( +g ` H ) , F ) ` n ) ) |
19 |
18
|
eqeq2d |
|- ( ph -> ( x = ( seq m ( ( +g ` G ) , F ) ` n ) <-> x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) |
20 |
19
|
anbi2d |
|- ( ph -> ( ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) <-> ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) ) |
21 |
20
|
rexbidv |
|- ( ph -> ( E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) <-> E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) ) |
22 |
21
|
exbidv |
|- ( ph -> ( E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) <-> E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) ) |
23 |
22
|
iotabidv |
|- ( ph -> ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) ) = ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) ) |
24 |
12
|
difeq2d |
|- ( ph -> ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) = ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) |
25 |
24
|
imaeq2d |
|- ( ph -> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) |
26 |
25
|
fveq2d |
|- ( ph -> ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) = ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) |
27 |
26
|
oveq2d |
|- ( ph -> ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) = ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) |
28 |
27
|
f1oeq2d |
|- ( ph -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) <-> f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) |
29 |
25
|
f1oeq3d |
|- ( ph -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) <-> f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) |
30 |
28 29
|
bitrd |
|- ( ph -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) <-> f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) |
31 |
5
|
seqeq2d |
|- ( ph -> seq 1 ( ( +g ` G ) , ( F o. f ) ) = seq 1 ( ( +g ` H ) , ( F o. f ) ) ) |
32 |
31 26
|
fveq12d |
|- ( ph -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) |
33 |
32
|
eqeq2d |
|- ( ph -> ( x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) <-> x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) |
34 |
30 33
|
anbi12d |
|- ( ph -> ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) ) <-> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) ) |
35 |
34
|
exbidv |
|- ( ph -> ( E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) ) <-> E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) ) |
36 |
35
|
iotabidv |
|- ( ph -> ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) ) ) = ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) ) |
37 |
23 36
|
ifeq12d |
|- ( ph -> if ( dom F e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) ) ) ) = if ( dom F e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) ) ) |
38 |
13 16 37
|
ifbieq12d |
|- ( ph -> if ( ran F C_ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } , ( 0g ` G ) , if ( dom F e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) ) ) ) ) = if ( ran F C_ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } , ( 0g ` H ) , if ( dom F e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) ) ) ) |
39 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
40 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
41 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
42 |
|
eqid |
|- { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } = { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } |
43 |
|
eqidd |
|- ( ph -> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) = ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) |
44 |
|
eqidd |
|- ( ph -> dom F = dom F ) |
45 |
39 40 41 42 43 2 1 44
|
gsumvalx |
|- ( ph -> ( G gsum F ) = if ( ran F C_ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } , ( 0g ` G ) , if ( dom F e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) ) ) ) ) ) ) ) |
46 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
47 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
48 |
|
eqid |
|- ( +g ` H ) = ( +g ` H ) |
49 |
|
eqid |
|- { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } = { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } |
50 |
|
eqidd |
|- ( ph -> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) |
51 |
46 47 48 49 50 3 1 44
|
gsumvalx |
|- ( ph -> ( H gsum F ) = if ( ran F C_ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } , ( 0g ` H ) , if ( dom F e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) ) ) ) ) ) ) ) |
52 |
38 45 51
|
3eqtr4d |
|- ( ph -> ( G gsum F ) = ( H gsum F ) ) |