Metamath Proof Explorer

Theorem gsumval3

Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised 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 gsumval3 
|- ( ph -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )

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 2 gsumz 
 |-  ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
14 5 6 13 syl2anc 
 |-  ( ph -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
15 14 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
16 7 feqmptd 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
17 16 adantr 
 |-  ( ( ph /\ W = (/) ) -> F = ( x e. A |-> ( F ` x ) ) )
18 f1f 
 |-  ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) --> A )
19 10 18 syl 
 |-  ( ph -> H : ( 1 ... M ) --> A )
20 19 ad2antrr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> H : ( 1 ... M ) --> A )
21 f1f1orn 
 |-  ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) -1-1-onto-> ran H )
22 10 21 syl 
 |-  ( ph -> H : ( 1 ... M ) -1-1-onto-> ran H )
23 22 adantr 
 |-  ( ( ph /\ W = (/) ) -> H : ( 1 ... M ) -1-1-onto-> ran H )
24 f1ocnv 
 |-  ( H : ( 1 ... M ) -1-1-onto-> ran H -> `' H : ran H -1-1-onto-> ( 1 ... M ) )
25 f1of 
 |-  ( `' H : ran H -1-1-onto-> ( 1 ... M ) -> `' H : ran H --> ( 1 ... M ) )
26 23 24 25 3syl 
 |-  ( ( ph /\ W = (/) ) -> `' H : ran H --> ( 1 ... M ) )
27 26 ffvelrnda 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( `' H ` x ) e. ( 1 ... M ) )
28 fvco3 
 |-  ( ( H : ( 1 ... M ) --> A /\ ( `' H ` x ) e. ( 1 ... M ) ) -> ( ( F o. H ) ` ( `' H ` x ) ) = ( F ` ( H ` ( `' H ` x ) ) ) )
29 20 27 28 syl2anc 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( ( F o. H ) ` ( `' H ` x ) ) = ( F ` ( H ` ( `' H ` x ) ) ) )
30 simpr 
 |-  ( ( ph /\ W = (/) ) -> W = (/) )
31 30 difeq2d 
 |-  ( ( ph /\ W = (/) ) -> ( ( 1 ... M ) \ W ) = ( ( 1 ... M ) \ (/) ) )
32 dif0 
 |-  ( ( 1 ... M ) \ (/) ) = ( 1 ... M )
33 31 32 eqtrdi 
 |-  ( ( ph /\ W = (/) ) -> ( ( 1 ... M ) \ W ) = ( 1 ... M ) )
34 33 adantr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( ( 1 ... M ) \ W ) = ( 1 ... M ) )
35 27 34 eleqtrrd 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( `' H ` x ) e. ( ( 1 ... M ) \ W ) )
36 fco 
 |-  ( ( F : A --> B /\ H : ( 1 ... M ) --> A ) -> ( F o. H ) : ( 1 ... M ) --> B )
37 7 19 36 syl2anc 
 |-  ( ph -> ( F o. H ) : ( 1 ... M ) --> B )
38 37 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( F o. H ) : ( 1 ... M ) --> B )
39 12 eqimss2i 
 |-  ( ( F o. H ) supp .0. ) C_ W
40 39 a1i 
 |-  ( ( ph /\ W = (/) ) -> ( ( F o. H ) supp .0. ) C_ W )
41 ovexd 
 |-  ( ( ph /\ W = (/) ) -> ( 1 ... M ) e. _V )
42 2 fvexi 
 |-  .0. e. _V
43 42 a1i 
 |-  ( ( ph /\ W = (/) ) -> .0. e. _V )
44 38 40 41 43 suppssr 
 |-  ( ( ( ph /\ W = (/) ) /\ ( `' H ` x ) e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` ( `' H ` x ) ) = .0. )
45 35 44 syldan 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( ( F o. H ) ` ( `' H ` x ) ) = .0. )
46 f1ocnvfv2 
 |-  ( ( H : ( 1 ... M ) -1-1-onto-> ran H /\ x e. ran H ) -> ( H ` ( `' H ` x ) ) = x )
47 23 46 sylan 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( H ` ( `' H ` x ) ) = x )
48 47 fveq2d 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( F ` ( H ` ( `' H ` x ) ) ) = ( F ` x ) )
49 29 45 48 3eqtr3rd 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( F ` x ) = .0. )
50 fvex 
 |-  ( F ` x ) e. _V
51 50 elsn 
 |-  ( ( F ` x ) e. { .0. } <-> ( F ` x ) = .0. )
52 49 51 sylibr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( F ` x ) e. { .0. } )
53 52 adantlr 
 |-  ( ( ( ( ph /\ W = (/) ) /\ x e. A ) /\ x e. ran H ) -> ( F ` x ) e. { .0. } )
54 eldif 
 |-  ( x e. ( A \ ran H ) <-> ( x e. A /\ -. x e. ran H ) )
55 42 a1i 
 |-  ( ph -> .0. e. _V )
56 7 11 6 55 suppssr 
 |-  ( ( ph /\ x e. ( A \ ran H ) ) -> ( F ` x ) = .0. )
57 56 51 sylibr 
 |-  ( ( ph /\ x e. ( A \ ran H ) ) -> ( F ` x ) e. { .0. } )
58 54 57 sylan2br 
 |-  ( ( ph /\ ( x e. A /\ -. x e. ran H ) ) -> ( F ` x ) e. { .0. } )
59 58 adantlr 
 |-  ( ( ( ph /\ W = (/) ) /\ ( x e. A /\ -. x e. ran H ) ) -> ( F ` x ) e. { .0. } )
60 59 anassrs 
 |-  ( ( ( ( ph /\ W = (/) ) /\ x e. A ) /\ -. x e. ran H ) -> ( F ` x ) e. { .0. } )
61 53 60 pm2.61dan 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. A ) -> ( F ` x ) e. { .0. } )
62 61 51 sylib 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. A ) -> ( F ` x ) = .0. )
63 62 mpteq2dva 
 |-  ( ( ph /\ W = (/) ) -> ( x e. A |-> ( F ` x ) ) = ( x e. A |-> .0. ) )
64 17 63 eqtrd 
 |-  ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
65 64 oveq2d 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum F ) = ( G gsum ( x e. A |-> .0. ) ) )
66 1 2 mndidcl 
 |-  ( G e. Mnd -> .0. e. B )
67 1 3 2 mndlid 
 |-  ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
68 5 66 67 syl2anc2 
 |-  ( ph -> ( .0. .+ .0. ) = .0. )
69 68 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
70 nnuz 
 |-  NN = ( ZZ>= ` 1 )
71 9 70 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
72 71 adantr 
 |-  ( ( ph /\ W = (/) ) -> M e. ( ZZ>= ` 1 ) )
73 33 eleq2d 
 |-  ( ( ph /\ W = (/) ) -> ( x e. ( ( 1 ... M ) \ W ) <-> x e. ( 1 ... M ) ) )
74 73 biimpar 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( 1 ... M ) ) -> x e. ( ( 1 ... M ) \ W ) )
75 38 40 41 43 suppssr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` x ) = .0. )
76 74 75 syldan 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. H ) ` x ) = .0. )
77 69 72 76 seqid3 
 |-  ( ( ph /\ W = (/) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = .0. )
78 15 65 77 3eqtr4d 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
79 fzf 
 |-  ... : ( ZZ X. ZZ ) --> ~P ZZ
80 ffn 
 |-  ( ... : ( ZZ X. ZZ ) --> ~P ZZ -> ... Fn ( ZZ X. ZZ ) )
81 ovelrn 
 |-  ( ... Fn ( ZZ X. ZZ ) -> ( A e. ran ... <-> E. m e. ZZ E. n e. ZZ A = ( m ... n ) ) )
82 79 80 81 mp2b 
 |-  ( A e. ran ... <-> E. m e. ZZ E. n e. ZZ A = ( m ... n ) )
83 5 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> G e. Mnd )
84 simpr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> A = ( m ... n ) )
85 frel 
 |-  ( F : A --> B -> Rel F )
86 reldm0 
 |-  ( Rel F -> ( F = (/) <-> dom F = (/) ) )
87 7 85 86 3syl 
 |-  ( ph -> ( F = (/) <-> dom F = (/) ) )
88 7 fdmd 
 |-  ( ph -> dom F = A )
89 88 eqeq1d 
 |-  ( ph -> ( dom F = (/) <-> A = (/) ) )
90 87 89 bitrd 
 |-  ( ph -> ( F = (/) <-> A = (/) ) )
91 coeq1 
 |-  ( F = (/) -> ( F o. H ) = ( (/) o. H ) )
92 co01 
 |-  ( (/) o. H ) = (/)
93 91 92 eqtrdi 
 |-  ( F = (/) -> ( F o. H ) = (/) )
94 93 oveq1d 
 |-  ( F = (/) -> ( ( F o. H ) supp .0. ) = ( (/) supp .0. ) )
95 supp0 
 |-  ( .0. e. _V -> ( (/) supp .0. ) = (/) )
96 42 95 ax-mp 
 |-  ( (/) supp .0. ) = (/)
97 94 96 eqtrdi 
 |-  ( F = (/) -> ( ( F o. H ) supp .0. ) = (/) )
98 12 97 syl5eq 
 |-  ( F = (/) -> W = (/) )
99 90 98 syl6bir 
 |-  ( ph -> ( A = (/) -> W = (/) ) )
100 99 necon3d 
 |-  ( ph -> ( W =/= (/) -> A =/= (/) ) )
101 100 imp 
 |-  ( ( ph /\ W =/= (/) ) -> A =/= (/) )
102 101 adantr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> A =/= (/) )
103 84 102 eqnetrrd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( m ... n ) =/= (/) )
104 fzn0 
 |-  ( ( m ... n ) =/= (/) <-> n e. ( ZZ>= ` m ) )
105 103 104 sylib 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> n e. ( ZZ>= ` m ) )
106 7 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> F : A --> B )
107 84 feq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( F : A --> B <-> F : ( m ... n ) --> B ) )
108 106 107 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> F : ( m ... n ) --> B )
109 1 3 83 105 108 gsumval2 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( G gsum F ) = ( seq m ( .+ , F ) ` n ) )
110 frn 
 |-  ( H : ( 1 ... M ) --> A -> ran H C_ A )
111 10 18 110 3syl 
 |-  ( ph -> ran H C_ A )
112 111 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H C_ A )
113 112 84 sseqtrd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H C_ ( m ... n ) )
114 fzssuz 
 |-  ( m ... n ) C_ ( ZZ>= ` m )
115 uzssz 
 |-  ( ZZ>= ` m ) C_ ZZ
116 zssre 
 |-  ZZ C_ RR
117 115 116 sstri 
 |-  ( ZZ>= ` m ) C_ RR
118 114 117 sstri 
 |-  ( m ... n ) C_ RR
119 113 118 sstrdi 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H C_ RR )
120 ltso 
 |-  < Or RR
121 soss 
 |-  ( ran H C_ RR -> ( < Or RR -> < Or ran H ) )
122 119 120 121 mpisyl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> < Or ran H )
123 fzfi 
 |-  ( 1 ... M ) e. Fin
124 123 a1i 
 |-  ( ph -> ( 1 ... M ) e. Fin )
125 fex2 
 |-  ( ( H : ( 1 ... M ) --> A /\ ( 1 ... M ) e. Fin /\ A e. V ) -> H e. _V )
126 19 124 6 125 syl3anc 
 |-  ( ph -> H e. _V )
127 f1oen3g 
 |-  ( ( H e. _V /\ H : ( 1 ... M ) -1-1-onto-> ran H ) -> ( 1 ... M ) ~~ ran H )
128 126 22 127 syl2anc 
 |-  ( ph -> ( 1 ... M ) ~~ ran H )
129 enfi 
 |-  ( ( 1 ... M ) ~~ ran H -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
130 128 129 syl 
 |-  ( ph -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
131 123 130 mpbii 
 |-  ( ph -> ran H e. Fin )
132 131 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H e. Fin )
133 fz1iso 
 |-  ( ( < Or ran H /\ ran H e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
134 122 132 133 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
135 9 nnnn0d 
 |-  ( ph -> M e. NN0 )
136 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
137 135 136 syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
138 124 22 hasheqf1od 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = ( # ` ran H ) )
139 137 138 eqtr3d 
 |-  ( ph -> M = ( # ` ran H ) )
140 139 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> M = ( # ` ran H ) )
141 140 fveq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. f ) ) ` M ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ran H ) ) )
142 5 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> G e. Mnd )
143 1 3 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
144 143 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
145 142 144 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
146 8 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran F C_ ( Z ` ran F ) )
147 146 sselda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ran F ) -> x e. ( Z ` ran F ) )
148 3 4 cntzi 
 |-  ( ( x e. ( Z ` ran F ) /\ y e. ran F ) -> ( x .+ y ) = ( y .+ x ) )
149 147 148 sylan 
 |-  ( ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ran F ) /\ y e. ran F ) -> ( x .+ y ) = ( y .+ x ) )
150 149 anasss 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. ran F /\ y e. ran F ) ) -> ( x .+ y ) = ( y .+ x ) )
151 1 3 mndass 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
152 142 151 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
153 71 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> M e. ( ZZ>= ` 1 ) )
154 7 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> F : A --> B )
155 154 frnd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran F C_ B )
156 simprr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
157 isof1o 
 |-  ( f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H )
158 156 157 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H )
159 140 oveq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( 1 ... M ) = ( 1 ... ( # ` ran H ) ) )
160 159 f1oeq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( f : ( 1 ... M ) -1-1-onto-> ran H <-> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H ) )
161 158 160 mpbird 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) -1-1-onto-> ran H )
162 f1ocnv 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ran H -> `' f : ran H -1-1-onto-> ( 1 ... M ) )
163 161 162 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> `' f : ran H -1-1-onto-> ( 1 ... M ) )
164 22 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H : ( 1 ... M ) -1-1-onto-> ran H )
165 f1oco 
 |-  ( ( `' f : ran H -1-1-onto-> ( 1 ... M ) /\ H : ( 1 ... M ) -1-1-onto-> ran H ) -> ( `' f o. H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
166 163 164 165 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( `' f o. H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
167 ffn 
 |-  ( F : A --> B -> F Fn A )
168 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
169 167 168 sylib 
 |-  ( F : A --> B -> F : A -onto-> ran F )
170 fof 
 |-  ( F : A -onto-> ran F -> F : A --> ran F )
171 154 169 170 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> F : A --> ran F )
172 f1of 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ran H -> f : ( 1 ... M ) --> ran H )
173 161 172 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) --> ran H )
174 111 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H C_ A )
175 173 174 fssd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) --> A )
176 fco 
 |-  ( ( F : A --> ran F /\ f : ( 1 ... M ) --> A ) -> ( F o. f ) : ( 1 ... M ) --> ran F )
177 171 175 176 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. f ) : ( 1 ... M ) --> ran F )
178 177 ffvelrnda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. f ) ` x ) e. ran F )
179 f1ococnv2 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ran H -> ( f o. `' f ) = ( _I |` ran H ) )
180 161 179 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( f o. `' f ) = ( _I |` ran H ) )
181 180 coeq1d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( f o. `' f ) o. H ) = ( ( _I |` ran H ) o. H ) )
182 f1of 
 |-  ( H : ( 1 ... M ) -1-1-onto-> ran H -> H : ( 1 ... M ) --> ran H )
183 fcoi2 
 |-  ( H : ( 1 ... M ) --> ran H -> ( ( _I |` ran H ) o. H ) = H )
184 164 182 183 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( _I |` ran H ) o. H ) = H )
185 181 184 eqtr2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H = ( ( f o. `' f ) o. H ) )
186 coass 
 |-  ( ( f o. `' f ) o. H ) = ( f o. ( `' f o. H ) )
187 185 186 eqtrdi 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H = ( f o. ( `' f o. H ) ) )
188 187 coeq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. H ) = ( F o. ( f o. ( `' f o. H ) ) ) )
189 coass 
 |-  ( ( F o. f ) o. ( `' f o. H ) ) = ( F o. ( f o. ( `' f o. H ) ) )
190 188 189 eqtr4di 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. H ) = ( ( F o. f ) o. ( `' f o. H ) ) )
191 190 fveq1d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( F o. H ) ` k ) = ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) )
192 191 adantr 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ k e. ( 1 ... M ) ) -> ( ( F o. H ) ` k ) = ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) )
193 f1of 
 |-  ( `' f : ran H -1-1-onto-> ( 1 ... M ) -> `' f : ran H --> ( 1 ... M ) )
194 161 162 193 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> `' f : ran H --> ( 1 ... M ) )
195 164 182 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H : ( 1 ... M ) --> ran H )
196 fco 
 |-  ( ( `' f : ran H --> ( 1 ... M ) /\ H : ( 1 ... M ) --> ran H ) -> ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) )
197 194 195 196 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) )
198 fvco3 
 |-  ( ( ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) /\ k e. ( 1 ... M ) ) -> ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) = ( ( F o. f ) ` ( ( `' f o. H ) ` k ) ) )
199 197 198 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ k e. ( 1 ... M ) ) -> ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) = ( ( F o. f ) ` ( ( `' f o. H ) ` k ) ) )
200 192 199 eqtrd 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ k e. ( 1 ... M ) ) -> ( ( F o. H ) ` k ) = ( ( F o. f ) ` ( ( `' f o. H ) ` k ) ) )
201 145 150 152 153 155 166 178 200 seqf1o 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq 1 ( .+ , ( F o. f ) ) ` M ) )
202 1 3 2 mndlid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( .0. .+ x ) = x )
203 142 202 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
204 1 3 2 mndrid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( x .+ .0. ) = x )
205 142 204 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. B ) -> ( x .+ .0. ) = x )
206 142 66 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> .0. e. B )
207 fdm 
 |-  ( H : ( 1 ... M ) --> A -> dom H = ( 1 ... M ) )
208 10 18 207 3syl 
 |-  ( ph -> dom H = ( 1 ... M ) )
209 eluzfz1 
 |-  ( M e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... M ) )
210 ne0i 
 |-  ( 1 e. ( 1 ... M ) -> ( 1 ... M ) =/= (/) )
211 71 209 210 3syl 
 |-  ( ph -> ( 1 ... M ) =/= (/) )
212 208 211 eqnetrd 
 |-  ( ph -> dom H =/= (/) )
213 dm0rn0 
 |-  ( dom H = (/) <-> ran H = (/) )
214 213 necon3bii 
 |-  ( dom H =/= (/) <-> ran H =/= (/) )
215 212 214 sylib 
 |-  ( ph -> ran H =/= (/) )
216 215 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H =/= (/) )
217 113 adantrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H C_ ( m ... n ) )
218 simprl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> A = ( m ... n ) )
219 218 eleq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( x e. A <-> x e. ( m ... n ) ) )
220 219 biimpar 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( m ... n ) ) -> x e. A )
221 154 ffvelrnda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. A ) -> ( F ` x ) e. B )
222 220 221 syldan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( m ... n ) ) -> ( F ` x ) e. B )
223 218 difeq1d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( A \ ran H ) = ( ( m ... n ) \ ran H ) )
224 223 eleq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( x e. ( A \ ran H ) <-> x e. ( ( m ... n ) \ ran H ) ) )
225 224 biimpar 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( ( m ... n ) \ ran H ) ) -> x e. ( A \ ran H ) )
226 56 ad4ant14 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( A \ ran H ) ) -> ( F ` x ) = .0. )
227 225 226 syldan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( ( m ... n ) \ ran H ) ) -> ( F ` x ) = .0. )
228 f1of 
 |-  ( f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H -> f : ( 1 ... ( # ` ran H ) ) --> ran H )
229 156 157 228 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... ( # ` ran H ) ) --> ran H )
230 fvco3 
 |-  ( ( f : ( 1 ... ( # ` ran H ) ) --> ran H /\ y e. ( 1 ... ( # ` ran H ) ) ) -> ( ( F o. f ) ` y ) = ( F ` ( f ` y ) ) )
231 229 230 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ y e. ( 1 ... ( # ` ran H ) ) ) -> ( ( F o. f ) ` y ) = ( F ` ( f ` y ) ) )
232 203 205 145 206 156 216 217 222 227 231 seqcoll2 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq m ( .+ , F ) ` n ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ran H ) ) )
233 141 201 232 3eqtr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) )
234 233 expr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) ) )
235 234 exlimdv 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) ) )
236 134 235 mpd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) )
237 109 236 eqtr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
238 237 ex 
 |-  ( ( ph /\ W =/= (/) ) -> ( A = ( m ... n ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
239 238 rexlimdvw 
 |-  ( ( ph /\ W =/= (/) ) -> ( E. n e. ZZ A = ( m ... n ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
240 239 rexlimdvw 
 |-  ( ( ph /\ W =/= (/) ) -> ( E. m e. ZZ E. n e. ZZ A = ( m ... n ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
241 82 240 syl5bi 
 |-  ( ( ph /\ W =/= (/) ) -> ( A e. ran ... -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
242 suppssdm 
 |-  ( ( F o. H ) supp .0. ) C_ dom ( F o. H )
243 12 242 eqsstri 
 |-  W C_ dom ( F o. H )
244 243 37 fssdm 
 |-  ( ph -> W C_ ( 1 ... M ) )
245 fz1ssnn 
 |-  ( 1 ... M ) C_ NN
246 nnssre 
 |-  NN C_ RR
247 245 246 sstri 
 |-  ( 1 ... M ) C_ RR
248 244 247 sstrdi 
 |-  ( ph -> W C_ RR )
249 soss 
 |-  ( W C_ RR -> ( < Or RR -> < Or W ) )
250 248 120 249 mpisyl 
 |-  ( ph -> < Or W )
251 ssfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ W C_ ( 1 ... M ) ) -> W e. Fin )
252 123 244 251 sylancr 
 |-  ( ph -> W e. Fin )
253 fz1iso 
 |-  ( ( < Or W /\ W e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
254 250 252 253 syl2anc 
 |-  ( ph -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
255 254 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
256 1 2 3 4 5 6 7 8 9 10 11 12 gsumval3lem2 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )
257 5 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> G e. Mnd )
258 257 202 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
259 257 204 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. B ) -> ( x .+ .0. ) = x )
260 257 144 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
261 257 66 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> .0. e. B )
262 simprr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
263 simplr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W =/= (/) )
264 244 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W C_ ( 1 ... M ) )
265 37 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F o. H ) : ( 1 ... M ) --> B )
266 265 ffvelrnda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. H ) ` x ) e. B )
267 39 a1i 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( F o. H ) supp .0. ) C_ W )
268 ovexd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( 1 ... M ) e. _V )
269 42 a1i 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> .0. e. _V )
270 265 267 268 269 suppssr 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` x ) = .0. )
271 coass 
 |-  ( ( F o. H ) o. f ) = ( F o. ( H o. f ) )
272 271 fveq1i 
 |-  ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. ( H o. f ) ) ` y )
273 isof1o 
 |-  ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
274 f1of 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) --> W )
275 262 273 274 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> W )
276 fvco3 
 |-  ( ( f : ( 1 ... ( # ` W ) ) --> W /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
277 275 276 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
278 272 277 syl5eqr 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. ( H o. f ) ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
279 258 259 260 261 262 263 264 266 270 278 seqcoll2 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )
280 256 279 eqtr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
281 280 expr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
282 281 exlimdv 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
283 255 282 mpd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
284 283 ex 
 |-  ( ( ph /\ W =/= (/) ) -> ( -. A e. ran ... -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
285 241 284 pm2.61d 
 |-  ( ( ph /\ W =/= (/) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
286 78 285 pm2.61dane 
 |-  ( ph -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )