Metamath Proof Explorer

Theorem gsumpropd2lem

Description: Lemma for gsumpropd2 . (Contributed by Thierry Arnoux, 28-Jun-2017)

Ref Expression
Hypotheses gsumpropd2.f 
|- ( ph -> F e. V )
gsumpropd2.g 
|- ( ph -> G e. W )
gsumpropd2.h 
|- ( ph -> H e. X )
gsumpropd2.b 
|- ( ph -> ( Base ` G ) = ( Base ` H ) )
gsumpropd2.c 
|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
gsumpropd2.e 
|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )
gsumpropd2.n 
|- ( ph -> Fun F )
gsumpropd2.r 
|- ( ph -> ran F C_ ( Base ` G ) )
gsumprop2dlem.1 
|- A = ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) )
gsumprop2dlem.2 
|- B = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) )
Assertion gsumpropd2lem 
|- ( ph -> ( G gsum F ) = ( H gsum F ) )

Proof

Step Hyp Ref Expression
1 gsumpropd2.f 
 |-  ( ph -> F e. V )
2 gsumpropd2.g 
 |-  ( ph -> G e. W )
3 gsumpropd2.h 
 |-  ( ph -> H e. X )
4 gsumpropd2.b 
 |-  ( ph -> ( Base ` G ) = ( Base ` H ) )
5 gsumpropd2.c 
 |-  ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
6 gsumpropd2.e 
 |-  ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )
7 gsumpropd2.n 
 |-  ( ph -> Fun F )
8 gsumpropd2.r 
 |-  ( ph -> ran F C_ ( Base ` G ) )
9 gsumprop2dlem.1 
 |-  A = ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) )
10 gsumprop2dlem.2 
 |-  B = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) )
11 4 adantr 
 |-  ( ( ph /\ s e. ( Base ` G ) ) -> ( Base ` G ) = ( Base ` H ) )
12 6 eqeq1d 
 |-  ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( ( s ( +g ` G ) t ) = t <-> ( s ( +g ` H ) t ) = t ) )
13 6 oveqrspc2v 
 |-  ( ( ph /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) = ( a ( +g ` H ) b ) )
14 13 oveqrspc2v 
 |-  ( ( ph /\ ( t e. ( Base ` G ) /\ s e. ( Base ` G ) ) ) -> ( t ( +g ` G ) s ) = ( t ( +g ` H ) s ) )
15 14 ancom2s 
 |-  ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( t ( +g ` G ) s ) = ( t ( +g ` H ) s ) )
16 15 eqeq1d 
 |-  ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( ( t ( +g ` G ) s ) = t <-> ( t ( +g ` H ) s ) = t ) )
17 12 16 anbi12d 
 |-  ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) <-> ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) ) )
18 17 anassrs 
 |-  ( ( ( ph /\ s e. ( Base ` G ) ) /\ t e. ( Base ` G ) ) -> ( ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) <-> ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) ) )
19 11 18 raleqbidva 
 |-  ( ( ph /\ s e. ( Base ` G ) ) -> ( 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 ) ) )
20 4 19 rabeqbidva 
 |-  ( 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 ) } )
21 20 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 ) } ) )
22 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
23 22 4 6 grpidpropd 
 |-  ( ph -> ( 0g ` G ) = ( 0g ` H ) )
24 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) -> n e. ( ZZ>= ` m ) )
25 8 ad2antrr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> ran F C_ ( Base ` G ) )
26 7 ad2antrr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> Fun F )
27 simpr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> s e. ( m ... n ) )
28 simplrr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> dom F = ( m ... n ) )
29 27 28 eleqtrrd 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> s e. dom F )
30 fvelrn 
 |-  ( ( Fun F /\ s e. dom F ) -> ( F ` s ) e. ran F )
31 26 29 30 syl2anc 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> ( F ` s ) e. ran F )
32 25 31 sseldd 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ s e. ( m ... n ) ) -> ( F ` s ) e. ( Base ` G ) )
33 5 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
34 6 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )
35 24 32 33 34 seqfeq4 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) -> ( seq m ( ( +g ` G ) , F ) ` n ) = ( seq m ( ( +g ` H ) , F ) ` n ) )
36 35 eqeq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` m ) /\ dom F = ( m ... n ) ) ) -> ( x = ( seq m ( ( +g ` G ) , F ) ` n ) <-> x = ( seq m ( ( +g ` H ) , F ) ` n ) ) )
37 36 anassrs 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` m ) ) /\ dom F = ( m ... n ) ) -> ( x = ( seq m ( ( +g ` G ) , F ) ` n ) <-> x = ( seq m ( ( +g ` H ) , F ) ` n ) ) )
38 37 pm5.32da 
 |-  ( ( ph /\ n e. ( ZZ>= ` m ) ) -> ( ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` G ) , F ) ` n ) ) <-> ( dom F = ( m ... n ) /\ x = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) )
39 38 rexbidva 
 |-  ( 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 ) ) ) )
40 39 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 ) ) ) )
41 40 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 ) ) ) )
42 20 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 ) } ) )
43 42 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 ) } ) ) )
44 43 9 10 3eqtr4g 
 |-  ( ph -> A = B )
45 44 fveq2d 
 |-  ( ph -> ( # ` A ) = ( # ` B ) )
46 45 fveq2d 
 |-  ( ph -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) )
47 46 adantr 
 |-  ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) )
48 simpr 
 |-  ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) -> ( # ` B ) e. ( ZZ>= ` 1 ) )
49 8 ad3antrrr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ran F C_ ( Base ` G ) )
50 f1ofun 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> Fun f )
51 50 ad3antlr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> Fun f )
52 simpr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> a e. ( 1 ... ( # ` B ) ) )
53 f1odm 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> dom f = ( 1 ... ( # ` A ) ) )
54 53 ad3antlr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> dom f = ( 1 ... ( # ` A ) ) )
55 45 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` A ) ) = ( 1 ... ( # ` B ) ) )
56 55 ad3antrrr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( 1 ... ( # ` A ) ) = ( 1 ... ( # ` B ) ) )
57 54 56 eqtrd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> dom f = ( 1 ... ( # ` B ) ) )
58 52 57 eleqtrrd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> a e. dom f )
59 fvco 
 |-  ( ( Fun f /\ a e. dom f ) -> ( ( F o. f ) ` a ) = ( F ` ( f ` a ) ) )
60 51 58 59 syl2anc 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( ( F o. f ) ` a ) = ( F ` ( f ` a ) ) )
61 7 ad3antrrr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> Fun F )
62 difpreima 
 |-  ( Fun F -> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) = ( ( `' F " _V ) \ ( `' F " { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) )
63 7 62 syl 
 |-  ( ph -> ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) = ( ( `' F " _V ) \ ( `' F " { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) )
64 9 63 eqtrid 
 |-  ( ph -> A = ( ( `' F " _V ) \ ( `' F " { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) )
65 difss 
 |-  ( ( `' F " _V ) \ ( `' F " { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) C_ ( `' F " _V )
66 64 65 eqsstrdi 
 |-  ( ph -> A C_ ( `' F " _V ) )
67 dfdm4 
 |-  dom F = ran `' F
68 dfrn4 
 |-  ran `' F = ( `' F " _V )
69 67 68 eqtri 
 |-  dom F = ( `' F " _V )
70 66 69 sseqtrrdi 
 |-  ( ph -> A C_ dom F )
71 70 ad3antrrr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> A C_ dom F )
72 f1of 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
73 72 ad3antlr 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
74 52 56 eleqtrrd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> a e. ( 1 ... ( # ` A ) ) )
75 73 74 ffvelrnd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( f ` a ) e. A )
76 71 75 sseldd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( f ` a ) e. dom F )
77 fvelrn 
 |-  ( ( Fun F /\ ( f ` a ) e. dom F ) -> ( F ` ( f ` a ) ) e. ran F )
78 61 76 77 syl2anc 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( F ` ( f ` a ) ) e. ran F )
79 60 78 eqeltrd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( ( F o. f ) ` a ) e. ran F )
80 49 79 sseldd 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ a e. ( 1 ... ( # ` B ) ) ) -> ( ( F o. f ) ` a ) e. ( Base ` G ) )
81 5 caovclg 
 |-  ( ( ph /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) e. ( Base ` G ) )
82 81 ad4ant14 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) e. ( Base ` G ) )
83 13 ad4ant14 
 |-  ( ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) ) -> ( a ( +g ` G ) b ) = ( a ( +g ` H ) b ) )
84 48 80 82 83 seqfeq4 
 |-  ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ ( # ` B ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) )
85 simpr 
 |-  ( ( ph /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> -. ( # ` B ) e. ( ZZ>= ` 1 ) )
86 1z 
 |-  1 e. ZZ
87 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( ( +g ` G ) , ( F o. f ) ) Fn ( ZZ>= ` 1 ) )
88 fndm 
 |-  ( seq 1 ( ( +g ` G ) , ( F o. f ) ) Fn ( ZZ>= ` 1 ) -> dom seq 1 ( ( +g ` G ) , ( F o. f ) ) = ( ZZ>= ` 1 ) )
89 86 87 88 mp2b 
 |-  dom seq 1 ( ( +g ` G ) , ( F o. f ) ) = ( ZZ>= ` 1 )
90 89 eleq2i 
 |-  ( ( # ` B ) e. dom seq 1 ( ( +g ` G ) , ( F o. f ) ) <-> ( # ` B ) e. ( ZZ>= ` 1 ) )
91 85 90 sylnibr 
 |-  ( ( ph /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> -. ( # ` B ) e. dom seq 1 ( ( +g ` G ) , ( F o. f ) ) )
92 ndmfv 
 |-  ( -. ( # ` B ) e. dom seq 1 ( ( +g ` G ) , ( F o. f ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) = (/) )
93 91 92 syl 
 |-  ( ( ph /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) = (/) )
94 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( ( +g ` H ) , ( F o. f ) ) Fn ( ZZ>= ` 1 ) )
95 fndm 
 |-  ( seq 1 ( ( +g ` H ) , ( F o. f ) ) Fn ( ZZ>= ` 1 ) -> dom seq 1 ( ( +g ` H ) , ( F o. f ) ) = ( ZZ>= ` 1 ) )
96 86 94 95 mp2b 
 |-  dom seq 1 ( ( +g ` H ) , ( F o. f ) ) = ( ZZ>= ` 1 )
97 96 eleq2i 
 |-  ( ( # ` B ) e. dom seq 1 ( ( +g ` H ) , ( F o. f ) ) <-> ( # ` B ) e. ( ZZ>= ` 1 ) )
98 85 97 sylnibr 
 |-  ( ( ph /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> -. ( # ` B ) e. dom seq 1 ( ( +g ` H ) , ( F o. f ) ) )
99 ndmfv 
 |-  ( -. ( # ` B ) e. dom seq 1 ( ( +g ` H ) , ( F o. f ) ) -> ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) = (/) )
100 98 99 syl 
 |-  ( ( ph /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) = (/) )
101 93 100 eqtr4d 
 |-  ( ( ph /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) )
102 101 adantlr 
 |-  ( ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ -. ( # ` B ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) )
103 84 102 pm2.61dan 
 |-  ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` B ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) )
104 47 103 eqtrd 
 |-  ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) )
105 104 eqeq2d 
 |-  ( ( ph /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) <-> x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) )
106 105 pm5.32da 
 |-  ( ph -> ( ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) <-> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) )
107 55 f1oeq2d 
 |-  ( ph -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> f : ( 1 ... ( # ` B ) ) -1-1-onto-> A ) )
108 44 f1oeq3d 
 |-  ( ph -> ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> A <-> f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) )
109 107 108 bitrd 
 |-  ( ph -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) )
110 109 anbi1d 
 |-  ( ph -> ( ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) <-> ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) )
111 106 110 bitrd 
 |-  ( ph -> ( ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) <-> ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) )
112 111 exbidv 
 |-  ( ph -> ( E. f ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) <-> E. f ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) )
113 112 iotabidv 
 |-  ( ph -> ( iota x E. f ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) ) = ( iota x E. f ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) )
114 41 113 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 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) ) ) = 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 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) ) )
115 21 23 114 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 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) ) ) ) = 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 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) ) ) )
116 eqid 
 |-  ( Base ` G ) = ( Base ` G )
117 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
118 eqid 
 |-  ( +g ` G ) = ( +g ` G )
119 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 ) }
120 9 a1i 
 |-  ( ph -> A = ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) )
121 eqidd 
 |-  ( ph -> dom F = dom F )
122 116 117 118 119 120 2 1 121 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 ... ( # ` A ) ) -1-1-onto-> A /\ x = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` A ) ) ) ) ) ) )
123 eqid 
 |-  ( Base ` H ) = ( Base ` H )
124 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
125 eqid 
 |-  ( +g ` H ) = ( +g ` H )
126 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 ) }
127 10 a1i 
 |-  ( ph -> B = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) )
128 123 124 125 126 127 3 1 121 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 ... ( # ` B ) ) -1-1-onto-> B /\ x = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` B ) ) ) ) ) ) )
129 115 122 128 3eqtr4d 
 |-  ( ph -> ( G gsum F ) = ( H gsum F ) )