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

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 ffvelcdmda 
 |-  ( ( ( 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 eqtrid 
 |-  ( F = (/) -> W = (/) )
99 90 98 biimtrrdi 
 |-  ( 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 19 124 fexd 
 |-  ( ph -> H e. _V )
126 f1oen3g 
 |-  ( ( H e. _V /\ H : ( 1 ... M ) -1-1-onto-> ran H ) -> ( 1 ... M ) ~~ ran H )
127 125 22 126 syl2anc 
 |-  ( ph -> ( 1 ... M ) ~~ ran H )
128 enfi 
 |-  ( ( 1 ... M ) ~~ ran H -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
129 127 128 syl 
 |-  ( ph -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
130 123 129 mpbii 
 |-  ( ph -> ran H e. Fin )
131 130 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H e. Fin )
132 fz1iso 
 |-  ( ( < Or ran H /\ ran H e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
133 122 131 132 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
134 9 nnnn0d 
 |-  ( ph -> M e. NN0 )
135 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
136 134 135 syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
137 124 22 hasheqf1od 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = ( # ` ran H ) )
138 136 137 eqtr3d 
 |-  ( ph -> M = ( # ` ran H ) )
139 138 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> M = ( # ` ran H ) )
140 139 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 ) ) )
141 5 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> G e. Mnd )
142 1 3 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
143 142 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
144 141 143 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
145 8 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran F C_ ( Z ` ran F ) )
146 145 sselda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ran F ) -> x e. ( Z ` ran F ) )
147 3 4 cntzi 
 |-  ( ( x e. ( Z ` ran F ) /\ y e. ran F ) -> ( x .+ y ) = ( y .+ x ) )
148 146 147 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 ) )
149 148 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 ) )
150 1 3 mndass 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
151 141 150 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 ) ) )
152 71 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> M e. ( ZZ>= ` 1 ) )
153 7 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> F : A --> B )
154 153 frnd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran F C_ B )
155 simprr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
156 isof1o 
 |-  ( f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H )
157 155 156 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H )
158 139 oveq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( 1 ... M ) = ( 1 ... ( # ` ran H ) ) )
159 158 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 ) )
160 157 159 mpbird 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) -1-1-onto-> ran H )
161 f1ocnv 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ran H -> `' f : ran H -1-1-onto-> ( 1 ... M ) )
162 160 161 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> `' f : ran H -1-1-onto-> ( 1 ... M ) )
163 22 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H : ( 1 ... M ) -1-1-onto-> ran H )
164 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 ) )
165 162 163 164 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( `' f o. H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
166 ffn 
 |-  ( F : A --> B -> F Fn A )
167 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
168 166 167 sylib 
 |-  ( F : A --> B -> F : A -onto-> ran F )
169 fof 
 |-  ( F : A -onto-> ran F -> F : A --> ran F )
170 153 168 169 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> F : A --> ran F )
171 f1of 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ran H -> f : ( 1 ... M ) --> ran H )
172 160 171 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) --> ran H )
173 111 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H C_ A )
174 172 173 fssd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) --> A )
175 fco 
 |-  ( ( F : A --> ran F /\ f : ( 1 ... M ) --> A ) -> ( F o. f ) : ( 1 ... M ) --> ran F )
176 170 174 175 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. f ) : ( 1 ... M ) --> ran F )
177 176 ffvelcdmda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. f ) ` x ) e. ran F )
178 f1ococnv2 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ran H -> ( f o. `' f ) = ( _I |` ran H ) )
179 160 178 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( f o. `' f ) = ( _I |` ran H ) )
180 179 coeq1d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( f o. `' f ) o. H ) = ( ( _I |` ran H ) o. H ) )
181 f1of 
 |-  ( H : ( 1 ... M ) -1-1-onto-> ran H -> H : ( 1 ... M ) --> ran H )
182 fcoi2 
 |-  ( H : ( 1 ... M ) --> ran H -> ( ( _I |` ran H ) o. H ) = H )
183 163 181 182 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( _I |` ran H ) o. H ) = H )
184 180 183 eqtr2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H = ( ( f o. `' f ) o. H ) )
185 coass 
 |-  ( ( f o. `' f ) o. H ) = ( f o. ( `' f o. H ) )
186 184 185 eqtrdi 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H = ( f o. ( `' f o. H ) ) )
187 186 coeq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. H ) = ( F o. ( f o. ( `' f o. H ) ) ) )
188 coass 
 |-  ( ( F o. f ) o. ( `' f o. H ) ) = ( F o. ( f o. ( `' f o. H ) ) )
189 187 188 eqtr4di 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. H ) = ( ( F o. f ) o. ( `' f o. H ) ) )
190 189 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 ) )
191 190 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 ) )
192 f1of 
 |-  ( `' f : ran H -1-1-onto-> ( 1 ... M ) -> `' f : ran H --> ( 1 ... M ) )
193 160 161 192 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> `' f : ran H --> ( 1 ... M ) )
194 163 181 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H : ( 1 ... M ) --> ran H )
195 fco 
 |-  ( ( `' f : ran H --> ( 1 ... M ) /\ H : ( 1 ... M ) --> ran H ) -> ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) )
196 193 194 195 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) )
197 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 ) ) )
198 196 197 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 ) ) )
199 191 198 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 ) ) )
200 144 149 151 152 154 165 177 199 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 ) )
201 1 3 2 mndlid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( .0. .+ x ) = x )
202 141 201 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
203 1 3 2 mndrid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( x .+ .0. ) = x )
204 141 203 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. B ) -> ( x .+ .0. ) = x )
205 141 66 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> .0. e. B )
206 fdm 
 |-  ( H : ( 1 ... M ) --> A -> dom H = ( 1 ... M ) )
207 10 18 206 3syl 
 |-  ( ph -> dom H = ( 1 ... M ) )
208 eluzfz1 
 |-  ( M e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... M ) )
209 ne0i 
 |-  ( 1 e. ( 1 ... M ) -> ( 1 ... M ) =/= (/) )
210 71 208 209 3syl 
 |-  ( ph -> ( 1 ... M ) =/= (/) )
211 207 210 eqnetrd 
 |-  ( ph -> dom H =/= (/) )
212 dm0rn0 
 |-  ( dom H = (/) <-> ran H = (/) )
213 212 necon3bii 
 |-  ( dom H =/= (/) <-> ran H =/= (/) )
214 211 213 sylib 
 |-  ( ph -> ran H =/= (/) )
215 214 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H =/= (/) )
216 113 adantrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H C_ ( m ... n ) )
217 simprl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> A = ( m ... n ) )
218 217 eleq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( x e. A <-> x e. ( m ... n ) ) )
219 218 biimpar 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( m ... n ) ) -> x e. A )
220 153 ffvelcdmda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. A ) -> ( F ` x ) e. B )
221 219 220 syldan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( m ... n ) ) -> ( F ` x ) e. B )
222 217 difeq1d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( A \ ran H ) = ( ( m ... n ) \ ran H ) )
223 222 eleq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( x e. ( A \ ran H ) <-> x e. ( ( m ... n ) \ ran H ) ) )
224 223 biimpar 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( ( m ... n ) \ ran H ) ) -> x e. ( A \ ran H ) )
225 56 ad4ant14 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( A \ ran H ) ) -> ( F ` x ) = .0. )
226 224 225 syldan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( ( m ... n ) \ ran H ) ) -> ( F ` x ) = .0. )
227 f1of 
 |-  ( f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H -> f : ( 1 ... ( # ` ran H ) ) --> ran H )
228 155 156 227 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... ( # ` ran H ) ) --> ran H )
229 fvco3 
 |-  ( ( f : ( 1 ... ( # ` ran H ) ) --> ran H /\ y e. ( 1 ... ( # ` ran H ) ) ) -> ( ( F o. f ) ` y ) = ( F ` ( f ` y ) ) )
230 228 229 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 ) ) )
231 202 204 144 205 155 215 216 221 226 230 seqcoll2 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq m ( .+ , F ) ` n ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ran H ) ) )
232 140 200 231 3eqtr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) )
233 232 expr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) ) )
234 233 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 ) ) )
235 133 234 mpd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) )
236 109 235 eqtr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
237 236 ex 
 |-  ( ( ph /\ W =/= (/) ) -> ( A = ( m ... n ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
238 237 rexlimdvw 
 |-  ( ( ph /\ W =/= (/) ) -> ( E. n e. ZZ A = ( m ... n ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
239 238 rexlimdvw 
 |-  ( ( ph /\ W =/= (/) ) -> ( E. m e. ZZ E. n e. ZZ A = ( m ... n ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
240 82 239 biimtrid 
 |-  ( ( ph /\ W =/= (/) ) -> ( A e. ran ... -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
241 suppssdm 
 |-  ( ( F o. H ) supp .0. ) C_ dom ( F o. H )
242 12 241 eqsstri 
 |-  W C_ dom ( F o. H )
243 242 37 fssdm 
 |-  ( ph -> W C_ ( 1 ... M ) )
244 fz1ssnn 
 |-  ( 1 ... M ) C_ NN
245 nnssre 
 |-  NN C_ RR
246 244 245 sstri 
 |-  ( 1 ... M ) C_ RR
247 243 246 sstrdi 
 |-  ( ph -> W C_ RR )
248 soss 
 |-  ( W C_ RR -> ( < Or RR -> < Or W ) )
249 247 120 248 mpisyl 
 |-  ( ph -> < Or W )
250 ssfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ W C_ ( 1 ... M ) ) -> W e. Fin )
251 123 243 250 sylancr 
 |-  ( ph -> W e. Fin )
252 fz1iso 
 |-  ( ( < Or W /\ W e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
253 249 251 252 syl2anc 
 |-  ( ph -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
254 253 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
255 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 ) ) )
256 5 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> G e. Mnd )
257 256 201 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
258 256 203 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. B ) -> ( x .+ .0. ) = x )
259 256 143 sylan 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
260 256 66 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> .0. e. B )
261 simprr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
262 simplr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W =/= (/) )
263 243 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W C_ ( 1 ... M ) )
264 37 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F o. H ) : ( 1 ... M ) --> B )
265 264 ffvelcdmda 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. H ) ` x ) e. B )
266 39 a1i 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( F o. H ) supp .0. ) C_ W )
267 ovexd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( 1 ... M ) e. _V )
268 42 a1i 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> .0. e. _V )
269 264 266 267 268 suppssr 
 |-  ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` x ) = .0. )
270 coass 
 |-  ( ( F o. H ) o. f ) = ( F o. ( H o. f ) )
271 270 fveq1i 
 |-  ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. ( H o. f ) ) ` y )
272 isof1o 
 |-  ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
273 f1of 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) --> W )
274 261 272 273 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> W )
275 fvco3 
 |-  ( ( f : ( 1 ... ( # ` W ) ) --> W /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
276 274 275 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 ) ) )
277 271 276 eqtr3id 
 |-  ( ( ( ( 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 257 258 259 260 261 262 263 265 269 277 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 ) ) )
279 255 278 eqtr4d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
280 279 expr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
281 280 exlimdv 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
282 254 281 mpd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
283 282 ex 
 |-  ( ( ph /\ W =/= (/) ) -> ( -. A e. ran ... -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
284 240 283 pm2.61d 
 |-  ( ( ph /\ W =/= (/) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
285 78 284 pm2.61dane 
 |-  ( ph -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )