This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumval3lem2

Description: Lemma 2 for gsumval3 . (Contributed by AV, 31-May-2019)

Ref Expression
Hypotheses gsumval3.b 
|- B = ( Base ` G )
gsumval3.0 
|- .0. = ( 0g ` G )
gsumval3.p 
|- .+ = ( +g ` G )
gsumval3.z 
|- Z = ( Cntz ` G )
gsumval3.g 
|- ( ph -> G e. Mnd )
gsumval3.a 
|- ( ph -> A e. V )
gsumval3.f 
|- ( ph -> F : A --> B )
gsumval3.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumval3.m 
|- ( ph -> M e. NN )
gsumval3.h 
|- ( ph -> H : ( 1 ... M ) -1-1-> A )
gsumval3.n 
|- ( ph -> ( F supp .0. ) C_ ran H )
gsumval3.w 
|- W = ( ( F o. H ) supp .0. )
Assertion gsumval3lem2 
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )

Proof

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 gsumval3.m 
 |-  ( ph -> M e. NN )
10 gsumval3.h 
 |-  ( ph -> H : ( 1 ... M ) -1-1-> A )
11 gsumval3.n 
 |-  ( ph -> ( F supp .0. ) C_ ran H )
12 gsumval3.w 
 |-  W = ( ( F o. H ) supp .0. )
13 f1f 
 |-  ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) --> A )
14 10 13 syl 
 |-  ( ph -> H : ( 1 ... M ) --> A )
15 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
16 14 15 fexd 
 |-  ( ph -> H e. _V )
17 vex 
 |-  f e. _V
18 coexg 
 |-  ( ( H e. _V /\ f e. _V ) -> ( H o. f ) e. _V )
19 16 17 18 sylancl 
 |-  ( ph -> ( H o. f ) e. _V )
20 19 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) e. _V )
21 1 2 3 4 5 6 7 8 9 10 11 12 gsumval3lem1 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) )
22 fzfi 
 |-  ( 1 ... M ) e. Fin
23 suppssdm 
 |-  ( ( F o. H ) supp .0. ) C_ dom ( F o. H )
24 12 23 eqsstri 
 |-  W C_ dom ( F o. H )
25 7 14 fcod 
 |-  ( ph -> ( F o. H ) : ( 1 ... M ) --> B )
26 24 25 fssdm 
 |-  ( ph -> W C_ ( 1 ... M ) )
27 ssfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ W C_ ( 1 ... M ) ) -> W e. Fin )
28 22 26 27 sylancr 
 |-  ( ph -> W e. Fin )
29 28 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W e. Fin )
30 10 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> H : ( 1 ... M ) -1-1-> A )
31 26 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W C_ ( 1 ... M ) )
32 f1ores 
 |-  ( ( H : ( 1 ... M ) -1-1-> A /\ W C_ ( 1 ... M ) ) -> ( H |` W ) : W -1-1-onto-> ( H " W ) )
33 30 31 32 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( H " W ) )
34 12 imaeq2i 
 |-  ( H " W ) = ( H " ( ( F o. H ) supp .0. ) )
35 7 6 fexd 
 |-  ( ph -> F e. _V )
36 ovex 
 |-  ( 1 ... M ) e. _V
37 fex 
 |-  ( ( H : ( 1 ... M ) --> A /\ ( 1 ... M ) e. _V ) -> H e. _V )
38 14 36 37 sylancl 
 |-  ( ph -> H e. _V )
39 35 38 jca 
 |-  ( ph -> ( F e. _V /\ H e. _V ) )
40 f1fun 
 |-  ( H : ( 1 ... M ) -1-1-> A -> Fun H )
41 10 40 syl 
 |-  ( ph -> Fun H )
42 41 11 jca 
 |-  ( ph -> ( Fun H /\ ( F supp .0. ) C_ ran H ) )
43 imacosupp 
 |-  ( ( F e. _V /\ H e. _V ) -> ( ( Fun H /\ ( F supp .0. ) C_ ran H ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) ) )
44 39 42 43 sylc 
 |-  ( ph -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) )
45 44 adantr 
 |-  ( ( ph /\ W =/= (/) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) )
46 34 45 eqtrid 
 |-  ( ( ph /\ W =/= (/) ) -> ( H " W ) = ( F supp .0. ) )
47 46 adantr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( F supp .0. ) )
48 47 f1oeq3d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H |` W ) : W -1-1-onto-> ( H " W ) <-> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) ) )
49 33 48 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) )
50 29 49 hasheqf1od 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( # ` W ) = ( # ` ( F supp .0. ) ) )
51 50 fveq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) )
52 21 51 jca 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) ) )
53 f1oeq1 
 |-  ( g = ( H o. f ) -> ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) <-> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) )
54 coeq2 
 |-  ( g = ( H o. f ) -> ( F o. g ) = ( F o. ( H o. f ) ) )
55 54 seqeq3d 
 |-  ( g = ( H o. f ) -> seq 1 ( .+ , ( F o. g ) ) = seq 1 ( .+ , ( F o. ( H o. f ) ) ) )
56 55 fveq1d 
 |-  ( g = ( H o. f ) -> ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) )
57 56 eqeq2d 
 |-  ( g = ( H o. f ) -> ( ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) <-> ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) ) )
58 53 57 anbi12d 
 |-  ( g = ( H o. f ) -> ( ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) ) ) )
59 20 52 58 spcedv 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) )
60 5 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> G e. Mnd )
61 6 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> A e. V )
62 7 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> F : A --> B )
63 8 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ran F C_ ( Z ` ran F ) )
64 f1f1orn 
 |-  ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) -1-1-onto-> ran H )
65 10 64 syl 
 |-  ( ph -> H : ( 1 ... M ) -1-1-onto-> ran H )
66 f1oen3g 
 |-  ( ( H e. _V /\ H : ( 1 ... M ) -1-1-onto-> ran H ) -> ( 1 ... M ) ~~ ran H )
67 16 65 66 syl2anc 
 |-  ( ph -> ( 1 ... M ) ~~ ran H )
68 enfi 
 |-  ( ( 1 ... M ) ~~ ran H -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
69 67 68 syl 
 |-  ( ph -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
70 22 69 mpbii 
 |-  ( ph -> ran H e. Fin )
71 70 11 ssfid 
 |-  ( ph -> ( F supp .0. ) e. Fin )
72 71 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F supp .0. ) e. Fin )
73 12 neeq1i 
 |-  ( W =/= (/) <-> ( ( F o. H ) supp .0. ) =/= (/) )
74 supp0cosupp0 
 |-  ( ( F e. _V /\ H e. _V ) -> ( ( F supp .0. ) = (/) -> ( ( F o. H ) supp .0. ) = (/) ) )
75 74 necon3d 
 |-  ( ( F e. _V /\ H e. _V ) -> ( ( ( F o. H ) supp .0. ) =/= (/) -> ( F supp .0. ) =/= (/) ) )
76 35 38 75 syl2anc 
 |-  ( ph -> ( ( ( F o. H ) supp .0. ) =/= (/) -> ( F supp .0. ) =/= (/) ) )
77 73 76 biimtrid 
 |-  ( ph -> ( W =/= (/) -> ( F supp .0. ) =/= (/) ) )
78 77 imp 
 |-  ( ( ph /\ W =/= (/) ) -> ( F supp .0. ) =/= (/) )
79 78 adantr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F supp .0. ) =/= (/) )
80 11 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F supp .0. ) C_ ran H )
81 14 frnd 
 |-  ( ph -> ran H C_ A )
82 81 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ran H C_ A )
83 80 82 sstrd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F supp .0. ) C_ A )
84 1 2 3 4 60 61 62 63 72 79 83 gsumval3eu 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> E! x E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) )
85 iota1 
 |-  ( E! x E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) -> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( iota x E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) ) = x ) )
86 84 85 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( iota x E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) ) = x ) )
87 eqid 
 |-  ( F supp .0. ) = ( F supp .0. )
88 simprl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> -. A e. ran ... )
89 1 2 3 4 60 61 62 63 72 79 87 88 gsumval3a 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsum F ) = ( iota x E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) ) )
90 89 eqeq1d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( G gsum F ) = x <-> ( iota x E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) ) = x ) )
91 86 90 bitr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = x ) )
92 91 alrimiv 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> A. x ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = x ) )
93 fvex 
 |-  ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) e. _V
94 eqeq1 
 |-  ( x = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) -> ( x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) <-> ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) )
95 94 anbi2d 
 |-  ( x = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) -> ( ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) ) )
96 95 exbidv 
 |-  ( x = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) -> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) ) )
97 eqeq2 
 |-  ( x = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) -> ( ( G gsum F ) = x <-> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) ) )
98 96 97 bibi12d 
 |-  ( x = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) -> ( ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = x ) <-> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) ) ) )
99 93 98 spcv 
 |-  ( A. x ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ x = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = x ) -> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) ) )
100 92 99 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( E. g ( g : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) /\ ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` ( F supp .0. ) ) ) ) <-> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) ) )
101 59 100 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )