Metamath Proof Explorer

Theorem gsumpropd

Description: The group sum depends only on the base set and additive operation. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd etc. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses gsumpropd.f 
|- ( ph -> F e. V )
gsumpropd.g 
|- ( ph -> G e. W )
gsumpropd.h 
|- ( ph -> H e. X )
gsumpropd.b 
|- ( ph -> ( Base ` G ) = ( Base ` H ) )
gsumpropd.p 
|- ( ph -> ( +g ` G ) = ( +g ` H ) )
Assertion gsumpropd 
|- ( ph -> ( G gsum F ) = ( H gsum F ) )

Proof

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