MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumval3 Unicode version

Theorem gsumval3 15191
Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.)
Hypotheses
Ref Expression
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 "
( _V  \  {  .0.  } ) )  C_  ran  H )
gsumval3.w  |-  W  =  ( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )
Assertion
Ref Expression
gsumval3  |-  ( ph  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) )

Proof of Theorem gsumval3
Dummy variables  f 
g  k  m  n  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumval3.g . . . . 5  |-  ( ph  ->  G  e.  Mnd )
2 gsumval3.a . . . . 5  |-  ( ph  ->  A  e.  V )
3 gsumval3.0 . . . . . 6  |-  .0.  =  ( 0g `  G )
43gsumz 14458 . . . . 5  |-  ( ( G  e.  Mnd  /\  A  e.  V )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
51, 2, 4syl2anc 642 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
65adantr 451 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
7 gsumval3.f . . . . . . 7  |-  ( ph  ->  F : A --> B )
87feqmptd 5575 . . . . . 6  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
98adantr 451 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
10 gsumval3.h . . . . . . . . . . . . . 14  |-  ( ph  ->  H : ( 1 ... M ) -1-1-> A
)
11 f1f 5437 . . . . . . . . . . . . . 14  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) --> A )
1210, 11syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  H : ( 1 ... M ) --> A )
1312ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  ->  H : ( 1 ... M ) --> A )
14 f1f1orn 5483 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
1510, 14syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  H : ( 1 ... M ) -1-1-onto-> ran  H
)
1615adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  H :
( 1 ... M
)
-1-1-onto-> ran  H )
17 f1ocnv 5485 . . . . . . . . . . . . . . 15  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' H : ran  H -1-1-onto-> ( 1 ... M ) )
1816, 17syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  `' H : ran  H -1-1-onto-> ( 1 ... M
) )
19 f1of 5472 . . . . . . . . . . . . . 14  |-  ( `' H : ran  H -1-1-onto-> (
1 ... M )  ->  `' H : ran  H --> ( 1 ... M
) )
2018, 19syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  `' H : ran  H --> ( 1 ... M ) )
21 ffvelrn 5663 . . . . . . . . . . . . 13  |-  ( ( `' H : ran  H --> ( 1 ... M
)  /\  x  e.  ran  H )  ->  ( `' H `  x )  e.  ( 1 ... M ) )
2220, 21sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( 1 ... M ) )
23 fvco3 5596 . . . . . . . . . . . 12  |-  ( ( H : ( 1 ... M ) --> A  /\  ( `' H `  x )  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `  ( H `  ( `' H `  x )
) ) )
2413, 22, 23syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `
 ( H `  ( `' H `  x ) ) ) )
25 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  W  =  (/) )  ->  W  =  (/) )
2625difeq2d 3294 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( ( 1 ... M
)  \  (/) ) )
27 dif0 3524 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M ) 
\  (/) )  =  ( 1 ... M )
2826, 27syl6eq 2331 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( 1 ... M ) )
2928adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( 1 ... M )  \  W
)  =  ( 1 ... M ) )
3022, 29eleqtrrd 2360 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( ( 1 ... M
)  \  W )
)
31 fco 5398 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> B  /\  H : ( 1 ... M ) --> A )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
327, 12, 31syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  o.  H
) : ( 1 ... M ) --> B )
3332adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
34 gsumval3.w . . . . . . . . . . . . . . 15  |-  W  =  ( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )
3534eqimss2i 3233 . . . . . . . . . . . . . 14  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  W
3635a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  W
)
3733, 36suppssr 5659 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  ( `' H `  x )  e.  ( ( 1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
3830, 37syldan 456 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
39 f1ocnvfv2 5793 . . . . . . . . . . . . 13  |-  ( ( H : ( 1 ... M ) -1-1-onto-> ran  H  /\  x  e.  ran  H )  ->  ( H `  ( `' H `  x ) )  =  x )
4016, 39sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( H `  ( `' H `  x ) )  =  x )
4140fveq2d 5529 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  ( H `  ( `' H `  x )
) )  =  ( F `  x ) )
4224, 38, 413eqtr3rd 2324 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  =  .0.  )
43 fvex 5539 . . . . . . . . . . 11  |-  ( F `
 x )  e. 
_V
4443elsnc 3663 . . . . . . . . . 10  |-  ( ( F `  x )  e.  {  .0.  }  <->  ( F `  x )  =  .0.  )
4542, 44sylibr 203 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  e.  {  .0.  } )
4645adantlr 695 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
47 eldif 3162 . . . . . . . . . . 11  |-  ( x  e.  ( A  \  ran  H )  <->  ( x  e.  A  /\  -.  x  e.  ran  H ) )
48 gsumval3.n . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
497, 48suppssr 5659 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  =  .0.  )
5049, 44sylibr 203 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  e.  {  .0.  } )
5147, 50sylan2br 462 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5251adantlr 695 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5352anassrs 629 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  -.  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
5446, 53pm2.61dan 766 . . . . . . 7  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  e.  {  .0.  } )
5554, 44sylib 188 . . . . . 6  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  =  .0.  )
5655mpteq2dva 4106 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  .0.  ) )
579, 56eqtrd 2315 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  .0.  ) )
5857oveq2d 5874 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  ( G 
gsumg  ( x  e.  A  |->  .0.  ) ) )
59 gsumval3.b . . . . . . . 8  |-  B  =  ( Base `  G
)
6059, 3mndidcl 14391 . . . . . . 7  |-  ( G  e.  Mnd  ->  .0.  e.  B )
611, 60syl 15 . . . . . 6  |-  ( ph  ->  .0.  e.  B )
62 gsumval3.p . . . . . . 7  |-  .+  =  ( +g  `  G )
6359, 62, 3mndlid 14393 . . . . . 6  |-  ( ( G  e.  Mnd  /\  .0.  e.  B )  -> 
(  .0.  .+  .0.  )  =  .0.  )
641, 61, 63syl2anc 642 . . . . 5  |-  ( ph  ->  (  .0.  .+  .0.  )  =  .0.  )
6564adantr 451 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  (  .0.  .+  .0.  )  =  .0.  )
66 gsumval3.m . . . . . 6  |-  ( ph  ->  M  e.  NN )
67 nnuz 10263 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
6866, 67syl6eleq 2373 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
6968adantr 451 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  M  e.  ( ZZ>= `  1 )
)
7028eleq2d 2350 . . . . . 6  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  ( ( 1 ... M )  \  W
)  <->  x  e.  (
1 ... M ) ) )
7170biimpar 471 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  x  e.  ( ( 1 ... M )  \  W
) )
7233, 36suppssr 5659 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( ( 1 ... M )  \  W
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7371, 72syldan 456 . . . 4  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7465, 69, 73seqid3 11090 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
)  =  .0.  )
756, 58, 743eqtr4d 2325 . 2  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
) )
76 fzf 10786 . . . . 5  |-  ... :
( ZZ  X.  ZZ )
--> ~P ZZ
77 ffn 5389 . . . . 5  |-  ( ...
: ( ZZ  X.  ZZ ) --> ~P ZZ  ->  ... 
Fn  ( ZZ  X.  ZZ ) )
78 ovelrn 5996 . . . . 5  |-  ( ... 
Fn  ( ZZ  X.  ZZ )  ->  ( A  e.  ran  ...  <->  E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n ) ) )
7976, 77, 78mp2b 9 . . . 4  |-  ( A  e.  ran  ...  <->  E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n ) )
801ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  G  e.  Mnd )
81 simpr 447 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =  ( m ... n ) )
82 frel 5392 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  Rel  F )
837, 82syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Rel  F )
84 reldm0 4896 . . . . . . . . . . . . . . . . 17  |-  ( Rel 
F  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
8583, 84syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
86 fdm 5393 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  dom  F  =  A )
877, 86syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  A )
8887eqeq1d 2291 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( dom  F  =  (/) 
<->  A  =  (/) ) )
8985, 88bitrd 244 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F  =  (/)  <->  A  =  (/) ) )
90 coeq1 4841 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  =  (/)  ->  ( F  o.  H )  =  ( (/)  o.  H
) )
91 co01 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  o.  H )  =  (/)
9290, 91syl6eq 2331 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  =  (/)  ->  ( F  o.  H )  =  (/) )
9392cnveqd 4857 . . . . . . . . . . . . . . . . . . 19  |-  ( F  =  (/)  ->  `' ( F  o.  H )  =  `' (/) )
94 cnv0 5084 . . . . . . . . . . . . . . . . . . 19  |-  `' (/)  =  (/)
9593, 94syl6eq 2331 . . . . . . . . . . . . . . . . . 18  |-  ( F  =  (/)  ->  `' ( F  o.  H )  =  (/) )
9695imaeq1d 5011 . . . . . . . . . . . . . . . . 17  |-  ( F  =  (/)  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  (
(/) " ( _V  \  {  .0.  } ) ) )
97 0ima 5031 . . . . . . . . . . . . . . . . 17  |-  ( (/) " ( _V  \  {  .0.  } ) )  =  (/)
9896, 97syl6eq 2331 . . . . . . . . . . . . . . . 16  |-  ( F  =  (/)  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  (/) )
9934, 98syl5eq 2327 . . . . . . . . . . . . . . 15  |-  ( F  =  (/)  ->  W  =  (/) )
10089, 99syl6bir 220 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  =  (/)  ->  W  =  (/) ) )
101100necon3d 2484 . . . . . . . . . . . . 13  |-  ( ph  ->  ( W  =/=  (/)  ->  A  =/=  (/) ) )
102101imp 418 . . . . . . . . . . . 12  |-  ( (
ph  /\  W  =/=  (/) )  ->  A  =/=  (/) )
103102adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =/=  (/) )
10481, 103eqnetrrd 2466 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( m ... n
)  =/=  (/) )
105 fzn0 10809 . . . . . . . . . 10  |-  ( ( m ... n )  =/=  (/)  <->  n  e.  ( ZZ>=
`  m ) )
106104, 105sylib 188 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  n  e.  ( ZZ>= `  m ) )
1077ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : A --> B )
10881feq2d 5380 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( F : A --> B 
<->  F : ( m ... n ) --> B ) )
109107, 108mpbid 201 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : ( m ... n ) --> B )
11059, 62, 80, 106, 109gsumval2 14460 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq  m (  .+  ,  F ) `  n
) )
111 frn 5395 . . . . . . . . . . . . . . 15  |-  ( H : ( 1 ... M ) --> A  ->  ran  H  C_  A )
11212, 111syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  C_  A
)
113112ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  A )
114113, 81sseqtrd 3214 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  ( m ... n ) )
115 fzssuz 10832 . . . . . . . . . . . . 13  |-  ( m ... n )  C_  ( ZZ>= `  m )
116 uzssz 10247 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  m )  C_  ZZ
117 zssre 10031 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
118116, 117sstri 3188 . . . . . . . . . . . . 13  |-  ( ZZ>= `  m )  C_  RR
119115, 118sstri 3188 . . . . . . . . . . . 12  |-  ( m ... n )  C_  RR
120114, 119syl6ss 3191 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  RR )
121 ltso 8903 . . . . . . . . . . 11  |-  <  Or  RR
122 soss 4332 . . . . . . . . . . 11  |-  ( ran 
H  C_  RR  ->  (  <  Or  RR  ->  < 
Or  ran  H )
)
123120, 121, 122ee10 1366 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  <  Or  ran  H )
124 fzfi 11034 . . . . . . . . . . . 12  |-  ( 1 ... M )  e. 
Fin
125124a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
126 fex2 5401 . . . . . . . . . . . . . . 15  |-  ( ( H : ( 1 ... M ) --> A  /\  ( 1 ... M )  e.  Fin  /\  A  e.  V )  ->  H  e.  _V )
12712, 125, 2, 126syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ph  ->  H  e.  _V )
128 f1oen3g 6877 . . . . . . . . . . . . . 14  |-  ( ( H  e.  _V  /\  H : ( 1 ... M ) -1-1-onto-> ran  H )  -> 
( 1 ... M
)  ~~  ran  H )
129127, 15, 128syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  ~~  ran  H )
130 enfi 7079 . . . . . . . . . . . . 13  |-  ( ( 1 ... M ) 
~~  ran  H  ->  ( ( 1 ... M
)  e.  Fin  <->  ran  H  e. 
Fin ) )
131129, 130syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... M )  e.  Fin  <->  ran  H  e.  Fin ) )
132124, 131mpbii 202 . . . . . . . . . . 11  |-  ( ph  ->  ran  H  e.  Fin )
133132ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  e.  Fin )
134 fz1iso 11400 . . . . . . . . . 10  |-  ( (  <  Or  ran  H  /\  ran  H  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
135123, 133, 134syl2anc 642 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
13666nnnn0d 10018 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  NN0 )
137 hashfz1 11345 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN0  ->  ( # `  ( 1 ... M
) )  =  M )
138136, 137syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  M )
139 hashen 11346 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ran  H  e.  Fin )  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
140124, 132, 139sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
141129, 140mpbird 223 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  ( # `  ran  H ) )
142138, 141eqtr3d 2317 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  =  ( # `  ran  H ) )
143142ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  =  ( # `  ran  H ) )
144143fveq2d 5529 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
1451ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  G  e.  Mnd )
14659, 62mndcl 14372 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  Mnd  /\  x  e.  B  /\  y  e.  B )  ->  ( x  .+  y
)  e.  B )
1471463expb 1152 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
148145, 147sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
149 gsumval3.c . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  F  C_  ( Z `  ran  F ) )
150149ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
151150sselda 3180 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ran  F )  ->  x  e.  ( Z `  ran  F
) )
152 gsumval3.z . . . . . . . . . . . . . . . 16  |-  Z  =  (Cntz `  G )
15362, 152cntzi 14805 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( Z `
 ran  F )  /\  y  e.  ran  F )  ->  ( x  .+  y )  =  ( y  .+  x ) )
154151, 153sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  (
m ... n )  /\  f  Isom  <  ,  <  ( ( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ran  F )  /\  y  e.  ran  F )  ->  ( x  .+  y )  =  ( y  .+  x ) )
155154anasss 628 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  ( x  e.  ran  F  /\  y  e.  ran  F ) )  ->  (
x  .+  y )  =  ( y  .+  x ) )
15659, 62mndass 14373 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B
) )  ->  (
( x  .+  y
)  .+  z )  =  ( x  .+  ( y  .+  z
) ) )
157145, 156sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
15868ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  e.  ( ZZ>= ` 
1 ) )
1597ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> B )
160 frn 5395 . . . . . . . . . . . . . 14  |-  ( F : A --> B  ->  ran  F  C_  B )
161159, 160syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  B )
162 simprr 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 ran  H )
) ,  ran  H
) )
163 isof1o 5822 . . . . . . . . . . . . . . . . 17  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
)  ->  f :
( 1 ... ( # `
 ran  H )
)
-1-1-onto-> ran  H )
164162, 163syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H )
165143oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( 1 ... M
)  =  ( 1 ... ( # `  ran  H ) ) )
166 f1oeq2 5464 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... M )  =  ( 1 ... ( # `  ran  H ) )  ->  (
f : ( 1 ... M ) -1-1-onto-> ran  H  <->  f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H ) )
167165, 166syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
168164, 167mpbird 223 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) -1-1-onto-> ran  H
)
169 f1ocnv 5485 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' f : ran  H -1-1-onto-> ( 1 ... M ) )
170168, 169syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  `' f : ran  H -1-1-onto-> ( 1 ... M ) )
17115ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
172 f1oco 5496 . . . . . . . . . . . . . 14  |-  ( ( `' 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 ) )
173170, 171, 172syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
174 ffn 5389 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  F  Fn  A )
175 dffn4 5457 . . . . . . . . . . . . . . . . . 18  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
176174, 175sylib 188 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> B  ->  F : A -onto-> ran  F
)
177159, 176syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A -onto-> ran  F
)
178 fof 5451 . . . . . . . . . . . . . . . 16  |-  ( F : A -onto-> ran  F  ->  F : A --> ran  F
)
179177, 178syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> ran  F
)
180 f1of 5472 . . . . . . . . . . . . . . . . 17  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  f : ( 1 ... M ) --> ran  H
)
181168, 180syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> ran 
H )
182112ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  A )
183 fss 5397 . . . . . . . . . . . . . . . 16  |-  ( ( f : ( 1 ... M ) --> ran 
H  /\  ran  H  C_  A )  ->  f : ( 1 ... M ) --> A )
184181, 182, 183syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> A )
185 fco 5398 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> ran  F  /\  f : ( 1 ... M ) --> A )  ->  ( F  o.  f ) : ( 1 ... M ) --> ran  F )
186179, 184, 185syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  f
) : ( 1 ... M ) --> ran 
F )
187 ffvelrn 5663 . . . . . . . . . . . . . 14  |-  ( ( ( F  o.  f
) : ( 1 ... M ) --> ran 
F  /\  x  e.  ( 1 ... M
) )  ->  (
( F  o.  f
) `  x )  e.  ran  F )
188186, 187sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( 1 ... M ) )  ->  ( ( F  o.  f ) `  x )  e.  ran  F )
189 f1ococnv2 5500 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  (
f  o.  `' f )  =  (  _I  |`  ran  H ) )
190168, 189syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( f  o.  `' f )  =  (  _I  |`  ran  H ) )
191190coeq1d 4845 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( ( f  o.  `' f )  o.  H )  =  ( (  _I  |`  ran  H
)  o.  H ) )
192 f1of 5472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  H : ( 1 ... M ) --> ran  H
)
193171, 192syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) --> ran  H
)
194 fcoi2 5416 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H : ( 1 ... M ) --> ran  H  ->  ( (  _I  |`  ran  H
)  o.  H )  =  H )
195193, 194syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( (  _I  |`  ran  H
)  o.  H )  =  H )
196191, 195eqtr2d 2316 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( (
f  o.  `' f )  o.  H ) )
197 coass 5191 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  o.  `' f )  o.  H )  =  ( f  o.  ( `' f  o.  H ) )
198196, 197syl6eq 2331 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( f  o.  ( `' f  o.  H ) ) )
199198coeq2d 4846 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( F  o.  ( f  o.  ( `' f  o.  H ) ) ) )
200 coass 5191 . . . . . . . . . . . . . . . . 17  |-  ( ( F  o.  f )  o.  ( `' f  o.  H ) )  =  ( F  o.  ( f  o.  ( `' f  o.  H
) ) )
201199, 200syl6eqr 2333 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( ( F  o.  f )  o.  ( `' f  o.  H ) ) )
202201fveq1d 5527 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( ( F  o.  H ) `  k
)  =  ( ( ( F  o.  f
)  o.  ( `' f  o.  H ) ) `  k ) )
203202adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) )
204 f1of 5472 . . . . . . . . . . . . . . . . 17  |-  ( `' f : ran  H -1-1-onto-> (
1 ... M )  ->  `' f : ran  H --> ( 1 ... M
) )
205170, 204syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  `' f : ran  H --> ( 1 ... M
) )
206 fco 5398 . . . . . . . . . . . . . . . 16  |-  ( ( `' f : ran  H --> ( 1 ... M
)  /\  H :
( 1 ... M
) --> ran  H )  ->  ( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
207205, 193, 206syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
208 fvco3 5596 . . . . . . . . . . . . . . 15  |-  ( ( ( `' 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 ) ) )
209207, 208sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
210203, 209eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) )
211148, 155, 157, 158, 161, 173, 188, 210seqf1o 11087 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq  1 ( 
.+  ,  ( F  o.  H ) ) `
 M )  =  (  seq  1 ( 
.+  ,  ( F  o.  f ) ) `
 M ) )
21259, 62, 3mndlid 14393 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
213145, 212sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
21459, 62, 3mndrid 14394 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
215145, 214sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
216145, 60syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  .0.  e.  B )
217 fdm 5393 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) --> A  ->  dom  H  =  ( 1 ... M ) )
21812, 217syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  H  =  ( 1 ... M ) )
219 eluzfz1 10803 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
22068, 219syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ( 1 ... M ) )
221 ne0i 3461 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
222220, 221syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
223218, 222eqnetrd 2464 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  H  =/=  (/) )
224 dm0rn0 4895 . . . . . . . . . . . . . . . 16  |-  ( dom 
H  =  (/)  <->  ran  H  =  (/) )
225224necon3bii 2478 . . . . . . . . . . . . . . 15  |-  ( dom 
H  =/=  (/)  <->  ran  H  =/=  (/) )
226223, 225sylib 188 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  =/=  (/) )
227226ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  =/=  (/) )
228114adantrr 697 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  ( m ... n ) )
229 simprl 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  A  =  ( m ... n ) )
230229eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  A  <->  x  e.  ( m ... n ) ) )
231230biimpar 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  ->  x  e.  A )
232 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> B  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
233159, 232sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
234231, 233syldan 456 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  -> 
( F `  x
)  e.  B )
235229difeq1d 3293 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( A  \  ran  H )  =  ( ( m ... n ) 
\  ran  H )
)
236235eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  ( A  \  ran  H
)  <->  x  e.  (
( m ... n
)  \  ran  H ) ) )
237236biimpar 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  ->  x  e.  ( A  \  ran  H ) )
238 simpll 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ph )
239238, 49sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( A  \  ran  H ) )  ->  ( F `  x )  =  .0.  )
240237, 239syldan 456 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  -> 
( F `  x
)  =  .0.  )
241 f1of 5472 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H  ->  f : ( 1 ... ( # `  ran  H ) ) --> ran  H
)
242164, 241syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... ( # `  ran  H ) ) --> ran  H
)
243 fvco3 5596 . . . . . . . . . . . . . 14  |-  ( ( f : ( 1 ... ( # `  ran  H ) ) --> ran  H  /\  y  e.  (
1 ... ( # `  ran  H ) ) )  -> 
( ( F  o.  f ) `  y
)  =  ( F `
 ( f `  y ) ) )
244242, 243sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  y  e.  ( 1 ... ( # `  ran  H ) ) )  -> 
( ( F  o.  f ) `  y
)  =  ( F `
 ( f `  y ) ) )
245213, 215, 148, 216, 162, 227, 228, 234, 240, 244seqcoll2 11402 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq  m (  .+  ,  F ) `  n )  =  (  seq  1 (  .+  ,  ( F  o.  f ) ) `  ( # `  ran  H
) ) )
246144, 211, 2453eqtr4d 2325 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq  1 ( 
.+  ,  ( F  o.  H ) ) `
 M )  =  (  seq  m ( 
.+  ,  F ) `
 n ) )
247246expr 598 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H )  ->  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
)  =  (  seq  m (  .+  ,  F ) `  n
) ) )
248247exlimdv 1664 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( E. f  f 
Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
)  ->  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
)  =  (  seq  m (  .+  ,  F ) `  n
) ) )
249135, 248mpd 14 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
(  seq  1 ( 
.+  ,  ( F  o.  H ) ) `
 M )  =  (  seq  m ( 
.+  ,  F ) `
 n ) )
250110, 249eqtr4d 2318 . . . . . . 7  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) )
251250ex 423 . . . . . 6  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
252251rexlimdvw 2670 . . . . 5  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
253252rexlimdvw 2670 . . . 4  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq  1
(  .+  ,  ( F  o.  H )
) `  M )
) )
25479, 253syl5bi 208 . . 3  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  e.  ran  ...  ->  ( G 
gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
255 cnvimass 5033 . . . . . . . . . . 11  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  dom  ( F  o.  H
)
25634, 255eqsstri 3208 . . . . . . . . . 10  |-  W  C_  dom  ( F  o.  H
)
257 fdm 5393 . . . . . . . . . . 11  |-  ( ( F  o.  H ) : ( 1 ... M ) --> B  ->  dom  ( F  o.  H
)  =  ( 1 ... M ) )
25832, 257syl 15 . . . . . . . . . 10  |-  ( ph  ->  dom  ( F  o.  H )  =  ( 1 ... M ) )
259256, 258syl5sseq 3226 . . . . . . . . 9  |-  ( ph  ->  W  C_  ( 1 ... M ) )
260 fzssuz 10832 . . . . . . . . . . 11  |-  ( 1 ... M )  C_  ( ZZ>= `  1 )
261260, 67sseqtr4i 3211 . . . . . . . . . 10  |-  ( 1 ... M )  C_  NN
262 nnssre 9750 . . . . . . . . . 10  |-  NN  C_  RR
263261, 262sstri 3188 . . . . . . . . 9  |-  ( 1 ... M )  C_  RR
264259, 263syl6ss 3191 . . . . . . . 8  |-  ( ph  ->  W  C_  RR )
265 soss 4332 . . . . . . . 8  |-  ( W 
C_  RR  ->  (  < 
Or  RR  ->  <  Or  W ) )
266264, 121, 265ee10 1366 . . . . . . 7  |-  ( ph  ->  <  Or  W )
267 ssfi 7083 . . . . . . . 8  |-  ( ( ( 1 ... M
)  e.  Fin  /\  W  C_  ( 1 ... M ) )  ->  W  e.  Fin )
268124, 259, 267sylancr 644 . . . . . . 7  |-  ( ph  ->  W  e.  Fin )
269 fz1iso 11400 . . . . . . 7  |-  ( (  <  Or  W  /\  W  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
270266, 268, 269syl2anc 642 . . . . . 6  |-  ( ph  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
271270ad2antrr 706 . . . . 5  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
272 vex 2791 . . . . . . . . . . . 12  |-  f  e. 
_V
273 coexg 5215 . . . . . . . . . . . 12  |-  ( ( H  e.  _V  /\  f  e.  _V )  ->  ( H  o.  f
)  e.  _V )
274127, 272, 273sylancl 643 . . . . . . . . . . 11  |-  ( ph  ->  ( H  o.  f
)  e.  _V )
275274ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
)  e.  _V )
27610ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -1-1-> A )
277259ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  C_  ( 1 ... M ) )
278 f1ores 5487 . . . . . . . . . . . . . . . 16  |-  ( ( H : ( 1 ... M ) -1-1-> A  /\  W  C_  ( 1 ... M ) )  ->  ( H  |`  W ) : W -1-1-onto-> ( H " W ) )
279276, 277, 278syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W ) : W -1-1-onto-> ( H " W
) )
280 cnvco 4865 . . . . . . . . . . . . . . . . . . . 20  |-  `' ( F  o.  H )  =  ( `' H  o.  `' F )
281280imaeq1i 5009 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  ( ( `' H  o.  `' F ) " ( _V  \  {  .0.  }
) )
282 imaco 5178 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' H  o.  `' F ) " ( _V  \  {  .0.  }
) )  =  ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) )
28334, 281, 2823eqtri 2307 . . . . . . . . . . . . . . . . . 18  |-  W  =  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )
284283imaeq2i 5010 . . . . . . . . . . . . . . . . 17  |-  ( H
" W )  =  ( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )
285276, 14syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
286 f1ofo 5479 . . . . . . . . . . . . . . . . . . 19  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  H : ( 1 ... M ) -onto-> ran  H
)
287285, 286syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -onto-> ran  H
)
28848ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
289 foimacnv 5490 . . . . . . . . . . . . . . . . . 18  |-  ( ( H : ( 1 ... M ) -onto-> ran 
H  /\  ( `' F " ( _V  \  {  .0.  } ) ) 
C_  ran  H )  ->  ( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )  =  ( `' F " ( _V  \  {  .0.  } ) ) )
290287, 288, 289syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )  =  ( `' F " ( _V  \  {  .0.  } ) ) )
291284, 290syl5eq 2327 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H " W
)  =  ( `' F " ( _V 
\  {  .0.  }
) ) )
292 f1oeq3 5465 . . . . . . . . . . . . . . . 16  |-  ( ( H " W )  =  ( `' F " ( _V  \  {  .0.  } ) )  -> 
( ( H  |`  W ) : W -1-1-onto-> ( H " W )  <->  ( H  |`  W ) : W -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) ) )
293291, 292syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 " ( _V 
\  {  .0.  }
) ) ) )
294279, 293mpbid 201 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
295 simprr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 W ) ) ,  W ) )
296 isof1o 5822 . . . . . . . . . . . . . . 15  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 W ) ) ,  W )  -> 
f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )
297295, 296syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )
298 f1oco 5496 . . . . . . . . . . . . . 14  |-  ( ( ( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )  ->  (
( H  |`  W )  o.  f ) : ( 1 ... ( # `
 W ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) )
299294, 297, 298syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( H  |`  W )  o.  f
) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
300 f1of 5472 . . . . . . . . . . . . . . . . 17  |-  ( f : ( 1 ... ( # `  W
) ) -1-1-onto-> W  ->  f :
( 1 ... ( # `
 W ) ) --> W )
301297, 300syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f : ( 1 ... ( # `  W
) ) --> W )
302 frn 5395 . . . . . . . . . . . . . . . 16  |-  ( f : ( 1 ... ( # `  W
) ) --> W  ->  ran  f  C_  W )
303301, 302syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  f  C_  W )
304 cores 5176 . . . . . . . . . . . . . . 15  |-  ( ran  f  C_  W  ->  ( ( H  |`  W )  o.  f )  =  ( H  o.  f
) )
305303, 304syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( H  |`  W )  o.  f
)  =  ( H  o.  f ) )
306 f1oeq1 5463 . . . . . . . . . . . . . 14  |-  ( ( ( H  |`  W )  o.  f )  =  ( H  o.  f
)  ->  ( (
( H  |`  W )  o.  f ) : ( 1 ... ( # `
 W ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  <->  ( H  o.  f ) : ( 1 ... ( # `  W ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) ) )
307305, 306syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( ( H  |`  W )  o.  f
) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  <->  ( H  o.  f ) : ( 1 ... ( # `  W ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) ) )
308299, 307mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
309 resexg 4994 . . . . . . . . . . . . . . . . . 18  |-  ( H  e.  _V  ->  ( H  |`  W )  e. 
_V )
310127, 309syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( H  |`  W )  e.  _V )
311310ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W )  e.  _V )
312 f1oen3g 6877 . . . . . . . . . . . . . . . 16  |-  ( ( ( H  |`  W )  e.  _V  /\  ( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )  ->  W  ~~  ( `' F " ( _V 
\  {  .0.  }
) ) )
313311, 294, 312syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  ~~  ( `' F " ( _V  \  {  .0.  } ) ) )
314268ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  e.  Fin )
315 ssfi 7083 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  H  e.  Fin  /\  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )  ->  ( `' F " ( _V 
\  {  .0.  }
) )  e.  Fin )
316132, 48, 315syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  e. 
Fin )
317316ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  e. 
Fin )
318 hashen 11346 . . . . . . . . . . . . . . . 16  |-  ( ( W  e.  Fin  /\  ( `' F " ( _V 
\  {  .0.  }
) )  e.  Fin )  ->  ( ( # `  W )  =  (
# `  ( `' F " ( _V  \  {  .0.  } ) ) )  <->  W  ~~  ( `' F " ( _V 
\  {  .0.  }
) ) ) )
319314, 317, 318syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( # `  W
)  =  ( # `  ( `' F "
( _V  \  {  .0.  } ) ) )  <-> 
W  ~~  ( `' F " ( _V  \  {  .0.  } ) ) ) )
320313, 319mpbird 223 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( # `  W )  =  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) )
321320oveq2d 5874 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( 1 ... ( # `
 W ) )  =  ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )
322 f1oeq2 5464 . . . . . . . . . . . . 13  |-  ( ( 1 ... ( # `  W ) )  =  ( 1 ... ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) )  ->  ( ( H  o.  f ) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  <->  ( H  o.  f ) : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) ) )
323321, 322syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( H  o.  f ) : ( 1 ... ( # `  W ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  <->  ( H  o.  f ) : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) ) )
324308, 323mpbid 201 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
) : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) )
325320fveq2d 5529 . . . . . . . . . . 11  |-  ( ( ( 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 " ( _V 
\  {  .0.  }
) ) ) ) )
326324, 325jca 518 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( H  o.  f ) : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) ) )
327 f1oeq1 5463 . . . . . . . . . . . 12  |-  ( g  =  ( H  o.  f )  ->  (
g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  <->  ( H  o.  f ) : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) ) )
328 coeq2 4842 . . . . . . . . . . . . . . 15  |-  ( g  =  ( H  o.  f )  ->  ( F  o.  g )  =  ( F  o.  ( H  o.  f
) ) )
329328seqeq3d 11054 . . . . . . . . . . . . . 14  |-  ( g  =  ( H  o.  f )  ->  seq  1 (  .+  , 
( F  o.  g
) )  =  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) )
330329fveq1d 5527 . . . . . . . . . . . . 13  |-  ( g  =  ( H  o.  f )  ->  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) )  =  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )
331330eqeq2d 2294 . . . . . . . . . . . 12  |-  ( g  =  ( H  o.  f )  ->  (
(  seq  1 ( 
.+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  =  (  seq  1 (  .+  ,  ( F  o.  g ) ) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) )  <-> 
(  seq  1 ( 
.+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  =  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) )
332327, 331anbi12d 691 . . . . . . . . . . 11  |-  ( g  =  ( H  o.  f )  ->  (
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( ( H  o.  f ) : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) )  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) ) )
333332spcegv 2869 . . . . . . . . . 10  |-  ( ( H  o.  f )  e.  _V  ->  (
( ( H  o.  f ) : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  ->  E. g
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) ) ) )
334275, 326, 333sylc 56 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  E. g ( g : ( 1 ... ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) ) )
3351ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  G  e.  Mnd )
3362ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  A  e.  V )
3377ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  F : A --> B )
338149ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
339 imaeq2 5008 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )  =  ( `' H "
(/) ) )
340 ima0 5030 . . . . . . . . . . . . . . . . . 18  |-  ( `' H " (/) )  =  (/)
341339, 340syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )  =  (/) )
342283, 341syl5eq 2327 . . . . . . . . . . . . . . . 16  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  W  =  (/) )
343342necon3i 2485 . . . . . . . . . . . . . . 15  |-  ( W  =/=  (/)  ->  ( `' F " ( _V  \  {  .0.  } ) )  =/=  (/) )
344343ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  =/=  (/) )
345112ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  H  C_  A )
346288, 345sstrd 3189 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  C_  A )
34759, 3, 62, 152, 335, 336, 337, 338, 317, 344, 346gsumval3eu 15190 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  E! x E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) )
348 iota1 5233 . . . . . . . . . . . . 13  |-  ( E! x E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )  ->  ( E. g ( g : ( 1 ... ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( iota x E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) )  =  x ) )
349347, 348syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )  <->  ( iota x E. g ( g : ( 1 ... ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) ) )  =  x ) )
350 eqid 2283 . . . . . . . . . . . . . 14  |-  ( `' F " ( _V 
\  {  .0.  }
) )  =  ( `' F " ( _V 
\  {  .0.  }
) )
351 simprl 732 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  -.  A  e.  ran  ... )
35259, 3, 62, 152, 335, 336, 337, 338, 317, 344, 350, 351gsumval3a 15189 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( G  gsumg  F )  =  ( iota x E. g
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) ) ) )
353352eqeq1d 2291 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( G  gsumg  F )  =  x  <->  ( iota x E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) )  =  x ) )
354349, 353bitr4d 247 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )  <->  ( G  gsumg  F )  =  x ) )
355354alrimiv 1617 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  A. x ( E. g
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( G  gsumg  F )  =  x ) )
356 fvex 5539 . . . . . . . . . . 11  |-  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) )  e.  _V
357 eqeq1 2289 . . . . . . . . . . . . . 14  |-  ( x  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  ->  (
x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) )  <->  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  =  (  seq  1 (  .+  ,  ( F  o.  g ) ) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) )
358357anbi2d 684 . . . . . . . . . . . . 13  |-  ( x  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  ->  (
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) )  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) ) ) )
359358exbidv 1612 . . . . . . . . . . . 12  |-  ( x  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  ->  ( E. g ( g : ( 1 ... ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  E. g
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) ) ) )
360 eqeq2 2292 . . . . . . . . . . . 12  |-  ( x  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  ->  (
( G  gsumg  F )  =  x  <-> 
( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) ) ) )
361359, 360bibi12d 312 . . . . . . . . . . 11  |-  ( x  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) )  ->  (
( E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  x  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )  <->  ( G  gsumg  F )  =  x )  <->  ( E. g ( g : ( 1 ... ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( G  gsumg  F )  =  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) ) ) ) )
362356, 361spcv 2874 . . . . . . . . . 10  |-  ( A. x ( E. g
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  x  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( G  gsumg  F )  =  x )  ->  ( E. g
( g : ( 1 ... ( # `  ( `' F "
( _V  \  {  .0.  } ) ) ) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) )  /\  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) )  =  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )  <->  ( G  gsumg  F )  =  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) ) ) )
363355, 362syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( E. g ( g : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) )  /\  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) )  =  (  seq  1
(  .+  ,  ( F  o.  g )
) `  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )  <->  ( G  gsumg  F )  =  (  seq  1
(  .+  ,  ( F  o.  ( H  o.  f ) ) ) `
 ( # `  W
) ) ) )
364334, 363mpbid 201 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) ) )
365335, 212sylan 457 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
366335, 214sylan 457 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
367335, 147sylan 457 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
368335, 60syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  .0.  e.  B )
369 simplr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
)