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

Theorem gsumval3 15514
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 14781 . . . . 5  |-  ( ( G  e.  Mnd  /\  A  e.  V )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
51, 2, 4syl2anc 643 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
65adantr 452 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
7 gsumval3.f . . . . . . 7  |-  ( ph  ->  F : A --> B )
87feqmptd 5779 . . . . . 6  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
98adantr 452 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
10 gsumval3.h . . . . . . . . . . . . . 14  |-  ( ph  ->  H : ( 1 ... M ) -1-1-> A
)
11 f1f 5639 . . . . . . . . . . . . . 14  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) --> A )
1210, 11syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  H : ( 1 ... M ) --> A )
1312ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  ->  H : ( 1 ... M ) --> A )
14 f1f1orn 5685 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
1510, 14syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  H : ( 1 ... M ) -1-1-onto-> ran  H
)
1615adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  H :
( 1 ... M
)
-1-1-onto-> ran  H )
17 f1ocnv 5687 . . . . . . . . . . . . . . 15  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' H : ran  H -1-1-onto-> ( 1 ... M ) )
1816, 17syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  `' H : ran  H -1-1-onto-> ( 1 ... M
) )
19 f1of 5674 . . . . . . . . . . . . . 14  |-  ( `' H : ran  H -1-1-onto-> (
1 ... M )  ->  `' H : ran  H --> ( 1 ... M
) )
2018, 19syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  `' H : ran  H --> ( 1 ... M ) )
2120ffvelrnda 5870 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( 1 ... M ) )
22 fvco3 5800 . . . . . . . . . . . 12  |-  ( ( H : ( 1 ... M ) --> A  /\  ( `' H `  x )  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `  ( H `  ( `' H `  x )
) ) )
2313, 21, 22syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `
 ( H `  ( `' H `  x ) ) ) )
24 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  W  =  (/) )  ->  W  =  (/) )
2524difeq2d 3465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( ( 1 ... M
)  \  (/) ) )
26 dif0 3698 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M ) 
\  (/) )  =  ( 1 ... M )
2725, 26syl6eq 2484 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( 1 ... M ) )
2827adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( 1 ... M )  \  W
)  =  ( 1 ... M ) )
2921, 28eleqtrrd 2513 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( ( 1 ... M
)  \  W )
)
30 fco 5600 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> B  /\  H : ( 1 ... M ) --> A )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
317, 12, 30syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  o.  H
) : ( 1 ... M ) --> B )
3231adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
33 gsumval3.w . . . . . . . . . . . . . . 15  |-  W  =  ( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )
3433eqimss2i 3403 . . . . . . . . . . . . . 14  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  W
3534a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  W
)
3632, 35suppssr 5864 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  ( `' H `  x )  e.  ( ( 1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
3729, 36syldan 457 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
38 f1ocnvfv2 6015 . . . . . . . . . . . . 13  |-  ( ( H : ( 1 ... M ) -1-1-onto-> ran  H  /\  x  e.  ran  H )  ->  ( H `  ( `' H `  x ) )  =  x )
3916, 38sylan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( H `  ( `' H `  x ) )  =  x )
4039fveq2d 5732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  ( H `  ( `' H `  x )
) )  =  ( F `  x ) )
4123, 37, 403eqtr3rd 2477 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  =  .0.  )
42 fvex 5742 . . . . . . . . . . 11  |-  ( F `
 x )  e. 
_V
4342elsnc 3837 . . . . . . . . . 10  |-  ( ( F `  x )  e.  {  .0.  }  <->  ( F `  x )  =  .0.  )
4441, 43sylibr 204 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  e.  {  .0.  } )
4544adantlr 696 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
46 eldif 3330 . . . . . . . . . . 11  |-  ( x  e.  ( A  \  ran  H )  <->  ( x  e.  A  /\  -.  x  e.  ran  H ) )
47 gsumval3.n . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
487, 47suppssr 5864 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  =  .0.  )
4948, 43sylibr 204 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  e.  {  .0.  } )
5046, 49sylan2br 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5150adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5251anassrs 630 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  -.  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
5345, 52pm2.61dan 767 . . . . . . 7  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  e.  {  .0.  } )
5453, 43sylib 189 . . . . . 6  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  =  .0.  )
5554mpteq2dva 4295 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  .0.  ) )
569, 55eqtrd 2468 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  .0.  ) )
5756oveq2d 6097 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  ( G 
gsumg  ( x  e.  A  |->  .0.  ) ) )
58 gsumval3.b . . . . . . . 8  |-  B  =  ( Base `  G
)
5958, 3mndidcl 14714 . . . . . . 7  |-  ( G  e.  Mnd  ->  .0.  e.  B )
601, 59syl 16 . . . . . 6  |-  ( ph  ->  .0.  e.  B )
61 gsumval3.p . . . . . . 7  |-  .+  =  ( +g  `  G )
6258, 61, 3mndlid 14716 . . . . . 6  |-  ( ( G  e.  Mnd  /\  .0.  e.  B )  -> 
(  .0.  .+  .0.  )  =  .0.  )
631, 60, 62syl2anc 643 . . . . 5  |-  ( ph  ->  (  .0.  .+  .0.  )  =  .0.  )
6463adantr 452 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  (  .0.  .+  .0.  )  =  .0.  )
65 gsumval3.m . . . . . 6  |-  ( ph  ->  M  e.  NN )
66 nnuz 10521 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
6765, 66syl6eleq 2526 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
6867adantr 452 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  M  e.  ( ZZ>= `  1 )
)
6927eleq2d 2503 . . . . . 6  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  ( ( 1 ... M )  \  W
)  <->  x  e.  (
1 ... M ) ) )
7069biimpar 472 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  x  e.  ( ( 1 ... M )  \  W
) )
7132, 35suppssr 5864 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( ( 1 ... M )  \  W
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7270, 71syldan 457 . . . 4  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7364, 68, 72seqid3 11367 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
)  =  .0.  )
746, 57, 733eqtr4d 2478 . 2  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
) )
75 fzf 11047 . . . . 5  |-  ... :
( ZZ  X.  ZZ )
--> ~P ZZ
76 ffn 5591 . . . . 5  |-  ( ...
: ( ZZ  X.  ZZ ) --> ~P ZZ  ->  ... 
Fn  ( ZZ  X.  ZZ ) )
77 ovelrn 6222 . . . . 5  |-  ( ... 
Fn  ( ZZ  X.  ZZ )  ->  ( A  e.  ran  ...  <->  E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n ) ) )
7875, 76, 77mp2b 10 . . . 4  |-  ( A  e.  ran  ...  <->  E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n ) )
791ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  G  e.  Mnd )
80 simpr 448 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =  ( m ... n ) )
81 frel 5594 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  Rel  F )
827, 81syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Rel  F )
83 reldm0 5087 . . . . . . . . . . . . . . . . 17  |-  ( Rel 
F  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
8482, 83syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
85 fdm 5595 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  dom  F  =  A )
867, 85syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  A )
8786eqeq1d 2444 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( dom  F  =  (/) 
<->  A  =  (/) ) )
8884, 87bitrd 245 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F  =  (/)  <->  A  =  (/) ) )
89 coeq1 5030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  =  (/)  ->  ( F  o.  H )  =  ( (/)  o.  H
) )
90 co01 5384 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  o.  H )  =  (/)
9189, 90syl6eq 2484 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  =  (/)  ->  ( F  o.  H )  =  (/) )
9291cnveqd 5048 . . . . . . . . . . . . . . . . . . 19  |-  ( F  =  (/)  ->  `' ( F  o.  H )  =  `' (/) )
93 cnv0 5275 . . . . . . . . . . . . . . . . . . 19  |-  `' (/)  =  (/)
9492, 93syl6eq 2484 . . . . . . . . . . . . . . . . . 18  |-  ( F  =  (/)  ->  `' ( F  o.  H )  =  (/) )
9594imaeq1d 5202 . . . . . . . . . . . . . . . . 17  |-  ( F  =  (/)  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  (
(/) " ( _V  \  {  .0.  } ) ) )
96 0ima 5222 . . . . . . . . . . . . . . . . 17  |-  ( (/) " ( _V  \  {  .0.  } ) )  =  (/)
9795, 96syl6eq 2484 . . . . . . . . . . . . . . . 16  |-  ( F  =  (/)  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  (/) )
9833, 97syl5eq 2480 . . . . . . . . . . . . . . 15  |-  ( F  =  (/)  ->  W  =  (/) )
9988, 98syl6bir 221 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  =  (/)  ->  W  =  (/) ) )
10099necon3d 2639 . . . . . . . . . . . . 13  |-  ( ph  ->  ( W  =/=  (/)  ->  A  =/=  (/) ) )
101100imp 419 . . . . . . . . . . . 12  |-  ( (
ph  /\  W  =/=  (/) )  ->  A  =/=  (/) )
102101adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =/=  (/) )
10380, 102eqnetrrd 2621 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( m ... n
)  =/=  (/) )
104 fzn0 11070 . . . . . . . . . 10  |-  ( ( m ... n )  =/=  (/)  <->  n  e.  ( ZZ>=
`  m ) )
105103, 104sylib 189 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  n  e.  ( ZZ>= `  m ) )
1067ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : A --> B )
10780feq2d 5581 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( F : A --> B 
<->  F : ( m ... n ) --> B ) )
108106, 107mpbid 202 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : ( m ... n ) --> B )
10958, 61, 79, 105, 108gsumval2 14783 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq  m (  .+  ,  F ) `  n
) )
110 frn 5597 . . . . . . . . . . . . . . 15  |-  ( H : ( 1 ... M ) --> A  ->  ran  H  C_  A )
11112, 110syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  C_  A
)
112111ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  A )
113112, 80sseqtrd 3384 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  ( m ... n ) )
114 fzssuz 11093 . . . . . . . . . . . . 13  |-  ( m ... n )  C_  ( ZZ>= `  m )
115 uzssz 10505 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  m )  C_  ZZ
116 zssre 10289 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
117115, 116sstri 3357 . . . . . . . . . . . . 13  |-  ( ZZ>= `  m )  C_  RR
118114, 117sstri 3357 . . . . . . . . . . . 12  |-  ( m ... n )  C_  RR
119113, 118syl6ss 3360 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  RR )
120 ltso 9156 . . . . . . . . . . 11  |-  <  Or  RR
121 soss 4521 . . . . . . . . . . 11  |-  ( ran 
H  C_  RR  ->  (  <  Or  RR  ->  < 
Or  ran  H )
)
122119, 120, 121ee10 1385 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  <  Or  ran  H )
123 fzfi 11311 . . . . . . . . . . . 12  |-  ( 1 ... M )  e. 
Fin
124123a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
125 fex2 5603 . . . . . . . . . . . . . . 15  |-  ( ( H : ( 1 ... M ) --> A  /\  ( 1 ... M )  e.  Fin  /\  A  e.  V )  ->  H  e.  _V )
12612, 124, 2, 125syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ph  ->  H  e.  _V )
127 f1oen3g 7123 . . . . . . . . . . . . . 14  |-  ( ( H  e.  _V  /\  H : ( 1 ... M ) -1-1-onto-> ran  H )  -> 
( 1 ... M
)  ~~  ran  H )
128126, 15, 127syl2anc 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  ~~  ran  H )
129 enfi 7325 . . . . . . . . . . . . 13  |-  ( ( 1 ... M ) 
~~  ran  H  ->  ( ( 1 ... M
)  e.  Fin  <->  ran  H  e. 
Fin ) )
130128, 129syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... M )  e.  Fin  <->  ran  H  e.  Fin ) )
131123, 130mpbii 203 . . . . . . . . . . 11  |-  ( ph  ->  ran  H  e.  Fin )
132131ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  e.  Fin )
133 fz1iso 11711 . . . . . . . . . 10  |-  ( (  <  Or  ran  H  /\  ran  H  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
134122, 132, 133syl2anc 643 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
13565nnnn0d 10274 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  NN0 )
136 hashfz1 11630 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN0  ->  ( # `  ( 1 ... M
) )  =  M )
137135, 136syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  M )
138 hashen 11631 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ran  H  e.  Fin )  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
139123, 131, 138sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
140128, 139mpbird 224 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  ( # `  ran  H ) )
141137, 140eqtr3d 2470 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  =  ( # `  ran  H ) )
142141ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  =  ( # `  ran  H ) )
143142fveq2d 5732 . . . . . . . . . . . 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 ) ) )
1441ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  G  e.  Mnd )
14558, 61mndcl 14695 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  Mnd  /\  x  e.  B  /\  y  e.  B )  ->  ( x  .+  y
)  e.  B )
1461453expb 1154 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
147144, 146sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
148 gsumval3.c . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  F  C_  ( Z `  ran  F ) )
149148ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
150149sselda 3348 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ran  F )  ->  x  e.  ( Z `  ran  F
) )
151 gsumval3.z . . . . . . . . . . . . . . . 16  |-  Z  =  (Cntz `  G )
15261, 151cntzi 15128 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( Z `
 ran  F )  /\  y  e.  ran  F )  ->  ( x  .+  y )  =  ( y  .+  x ) )
153150, 152sylan 458 . . . . . . . . . . . . . 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 ) )
154153anasss 629 . . . . . . . . . . . . 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 ) )
15558, 61mndass 14696 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B
) )  ->  (
( x  .+  y
)  .+  z )  =  ( x  .+  ( y  .+  z
) ) )
156144, 155sylan 458 . . . . . . . . . . . . 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
) ) )
15767ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  e.  ( ZZ>= ` 
1 ) )
1587ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> B )
159 frn 5597 . . . . . . . . . . . . . 14  |-  ( F : A --> B  ->  ran  F  C_  B )
160158, 159syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  B )
161 simprr 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 ran  H )
) ,  ran  H
) )
162 isof1o 6045 . . . . . . . . . . . . . . . . 17  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
)  ->  f :
( 1 ... ( # `
 ran  H )
)
-1-1-onto-> ran  H )
163161, 162syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H )
164142oveq2d 6097 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( 1 ... M
)  =  ( 1 ... ( # `  ran  H ) ) )
165 f1oeq2 5666 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... M )  =  ( 1 ... ( # `  ran  H ) )  ->  (
f : ( 1 ... M ) -1-1-onto-> ran  H  <->  f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H ) )
166164, 165syl 16 . . . . . . . . . . . . . . . 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 ) )
167163, 166mpbird 224 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) -1-1-onto-> ran  H
)
168 f1ocnv 5687 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' f : ran  H -1-1-onto-> ( 1 ... M ) )
169167, 168syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  `' f : ran  H -1-1-onto-> ( 1 ... M ) )
17015ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
171 f1oco 5698 . . . . . . . . . . . . . 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 ) )
172169, 170, 171syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
173 ffn 5591 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  F  Fn  A )
174 dffn4 5659 . . . . . . . . . . . . . . . . . 18  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
175173, 174sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> B  ->  F : A -onto-> ran  F
)
176158, 175syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A -onto-> ran  F
)
177 fof 5653 . . . . . . . . . . . . . . . 16  |-  ( F : A -onto-> ran  F  ->  F : A --> ran  F
)
178176, 177syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> ran  F
)
179 f1of 5674 . . . . . . . . . . . . . . . . 17  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  f : ( 1 ... M ) --> ran  H
)
180167, 179syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> ran 
H )
181111ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  A )
182 fss 5599 . . . . . . . . . . . . . . . 16  |-  ( ( f : ( 1 ... M ) --> ran 
H  /\  ran  H  C_  A )  ->  f : ( 1 ... M ) --> A )
183180, 181, 182syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> A )
184 fco 5600 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> ran  F  /\  f : ( 1 ... M ) --> A )  ->  ( F  o.  f ) : ( 1 ... M ) --> ran  F )
185178, 183, 184syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  f
) : ( 1 ... M ) --> ran 
F )
186185ffvelrnda 5870 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( 1 ... M ) )  ->  ( ( F  o.  f ) `  x )  e.  ran  F )
187 f1ococnv2 5702 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  (
f  o.  `' f )  =  (  _I  |`  ran  H ) )
188167, 187syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( f  o.  `' f )  =  (  _I  |`  ran  H ) )
189188coeq1d 5034 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( ( f  o.  `' f )  o.  H )  =  ( (  _I  |`  ran  H
)  o.  H ) )
190 f1of 5674 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  H : ( 1 ... M ) --> ran  H
)
191170, 190syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) --> ran  H
)
192 fcoi2 5618 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H : ( 1 ... M ) --> ran  H  ->  ( (  _I  |`  ran  H
)  o.  H )  =  H )
193191, 192syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( (  _I  |`  ran  H
)  o.  H )  =  H )
194189, 193eqtr2d 2469 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( (
f  o.  `' f )  o.  H ) )
195 coass 5388 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  o.  `' f )  o.  H )  =  ( f  o.  ( `' f  o.  H ) )
196194, 195syl6eq 2484 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( f  o.  ( `' f  o.  H ) ) )
197196coeq2d 5035 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( F  o.  ( f  o.  ( `' f  o.  H ) ) ) )
198 coass 5388 . . . . . . . . . . . . . . . . 17  |-  ( ( F  o.  f )  o.  ( `' f  o.  H ) )  =  ( F  o.  ( f  o.  ( `' f  o.  H
) ) )
199197, 198syl6eqr 2486 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( ( F  o.  f )  o.  ( `' f  o.  H ) ) )
200199fveq1d 5730 . . . . . . . . . . . . . . 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 ) )
201200adantr 452 . . . . . . . . . . . . . 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
) )
202 f1of 5674 . . . . . . . . . . . . . . . . 17  |-  ( `' f : ran  H -1-1-onto-> (
1 ... M )  ->  `' f : ran  H --> ( 1 ... M
) )
203169, 202syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  `' f : ran  H --> ( 1 ... M
) )
204 fco 5600 . . . . . . . . . . . . . . . 16  |-  ( ( `' f : ran  H --> ( 1 ... M
)  /\  H :
( 1 ... M
) --> ran  H )  ->  ( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
205203, 191, 204syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
206 fvco3 5800 . . . . . . . . . . . . . . 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 ) ) )
207205, 206sylan 458 . . . . . . . . . . . . . 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
) ) )
208201, 207eqtrd 2468 . . . . . . . . . . . . 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 )
) )
209147, 154, 156, 157, 160, 172, 186, 208seqf1o 11364 . . . . . . . . . . . 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 ) )
21058, 61, 3mndlid 14716 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
211144, 210sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
21258, 61, 3mndrid 14717 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
213144, 212sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
214144, 59syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  .0.  e.  B )
215 fdm 5595 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) --> A  ->  dom  H  =  ( 1 ... M ) )
21612, 215syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  H  =  ( 1 ... M ) )
217 eluzfz1 11064 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
21867, 217syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ( 1 ... M ) )
219 ne0i 3634 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
220218, 219syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
221216, 220eqnetrd 2619 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  H  =/=  (/) )
222 dm0rn0 5086 . . . . . . . . . . . . . . . 16  |-  ( dom 
H  =  (/)  <->  ran  H  =  (/) )
223222necon3bii 2633 . . . . . . . . . . . . . . 15  |-  ( dom 
H  =/=  (/)  <->  ran  H  =/=  (/) )
224221, 223sylib 189 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  =/=  (/) )
225224ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  =/=  (/) )
226113adantrr 698 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  ( m ... n ) )
227 simprl 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  A  =  ( m ... n ) )
228227eleq2d 2503 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  A  <->  x  e.  ( m ... n ) ) )
229228biimpar 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  ->  x  e.  A )
230158ffvelrnda 5870 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
231229, 230syldan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  -> 
( F `  x
)  e.  B )
232227difeq1d 3464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( A  \  ran  H )  =  ( ( m ... n ) 
\  ran  H )
)
233232eleq2d 2503 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  ( A  \  ran  H
)  <->  x  e.  (
( m ... n
)  \  ran  H ) ) )
234233biimpar 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  ->  x  e.  ( A  \  ran  H ) )
235 simpll 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ph )
236235, 48sylan 458 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( A  \  ran  H ) )  ->  ( F `  x )  =  .0.  )
237234, 236syldan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  -> 
( F `  x
)  =  .0.  )
238 f1of 5674 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H  ->  f : ( 1 ... ( # `  ran  H ) ) --> ran  H
)
239163, 238syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... ( # `  ran  H ) ) --> ran  H
)
240 fvco3 5800 . . . . . . . . . . . . . 14  |-  ( ( f : ( 1 ... ( # `  ran  H ) ) --> ran  H  /\  y  e.  (
1 ... ( # `  ran  H ) ) )  -> 
( ( F  o.  f ) `  y
)  =  ( F `
 ( f `  y ) ) )
241239, 240sylan 458 . . . . . . . . . . . . 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 ) ) )
242211, 213, 147, 214, 161, 225, 226, 231, 237, 241seqcoll2 11713 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq  m (  .+  ,  F ) `  n )  =  (  seq  1 (  .+  ,  ( F  o.  f ) ) `  ( # `  ran  H
) ) )
243143, 209, 2423eqtr4d 2478 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq  1 ( 
.+  ,  ( F  o.  H ) ) `
 M )  =  (  seq  m ( 
.+  ,  F ) `
 n ) )
244243expr 599 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H )  ->  (  seq  1 (  .+  , 
( F  o.  H
) ) `  M
)  =  (  seq  m (  .+  ,  F ) `  n
) ) )
245244exlimdv 1646 . . . . . . . . 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
) ) )
246134, 245mpd 15 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
(  seq  1 ( 
.+  ,  ( F  o.  H ) ) `
 M )  =  (  seq  m ( 
.+  ,  F ) `
 n ) )
247109, 246eqtr4d 2471 . . . . . . 7  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) )
248247ex 424 . . . . . 6  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
249248rexlimdvw 2833 . . . . 5  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
250249rexlimdvw 2833 . . . 4  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq  1
(  .+  ,  ( F  o.  H )
) `  M )
) )
25178, 250syl5bi 209 . . 3  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  e.  ran  ...  ->  ( G 
gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
252 cnvimass 5224 . . . . . . . . . . 11  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  dom  ( F  o.  H
)
25333, 252eqsstri 3378 . . . . . . . . . 10  |-  W  C_  dom  ( F  o.  H
)
254 fdm 5595 . . . . . . . . . . 11  |-  ( ( F  o.  H ) : ( 1 ... M ) --> B  ->  dom  ( F  o.  H
)  =  ( 1 ... M ) )
25531, 254syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  ( F  o.  H )  =  ( 1 ... M ) )
256253, 255syl5sseq 3396 . . . . . . . . 9  |-  ( ph  ->  W  C_  ( 1 ... M ) )
257 fzssuz 11093 . . . . . . . . . . 11  |-  ( 1 ... M )  C_  ( ZZ>= `  1 )
258257, 66sseqtr4i 3381 . . . . . . . . . 10  |-  ( 1 ... M )  C_  NN
259 nnssre 10004 . . . . . . . . . 10  |-  NN  C_  RR
260258, 259sstri 3357 . . . . . . . . 9  |-  ( 1 ... M )  C_  RR
261256, 260syl6ss 3360 . . . . . . . 8  |-  ( ph  ->  W  C_  RR )
262 soss 4521 . . . . . . . 8  |-  ( W 
C_  RR  ->  (  < 
Or  RR  ->  <  Or  W ) )
263261, 120, 262ee10 1385 . . . . . . 7  |-  ( ph  ->  <  Or  W )
264 ssfi 7329 . . . . . . . 8  |-  ( ( ( 1 ... M
)  e.  Fin  /\  W  C_  ( 1 ... M ) )  ->  W  e.  Fin )
265123, 256, 264sylancr 645 . . . . . . 7  |-  ( ph  ->  W  e.  Fin )
266 fz1iso 11711 . . . . . . 7  |-  ( (  <  Or  W  /\  W  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
267263, 265, 266syl2anc 643 . . . . . 6  |-  ( ph  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
268267ad2antrr 707 . . . . 5  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
269 vex 2959 . . . . . . . . . . . 12  |-  f  e. 
_V
270 coexg 5412 . . . . . . . . . . . 12  |-  ( ( H  e.  _V  /\  f  e.  _V )  ->  ( H  o.  f
)  e.  _V )
271126, 269, 270sylancl 644 . . . . . . . . . . 11  |-  ( ph  ->  ( H  o.  f
)  e.  _V )
272271ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
)  e.  _V )
27310ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -1-1-> A )
274256ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  C_  ( 1 ... M ) )
275 f1ores 5689 . . . . . . . . . . . . . . . 16  |-  ( ( H : ( 1 ... M ) -1-1-> A  /\  W  C_  ( 1 ... M ) )  ->  ( H  |`  W ) : W -1-1-onto-> ( H " W ) )
276273, 274, 275syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W ) : W -1-1-onto-> ( H " W
) )
277 cnvco 5056 . . . . . . . . . . . . . . . . . . . 20  |-  `' ( F  o.  H )  =  ( `' H  o.  `' F )
278277imaeq1i 5200 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  ( ( `' H  o.  `' F ) " ( _V  \  {  .0.  }
) )
279 imaco 5375 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' H  o.  `' F ) " ( _V  \  {  .0.  }
) )  =  ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) )
28033, 278, 2793eqtri 2460 . . . . . . . . . . . . . . . . . 18  |-  W  =  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )
281280imaeq2i 5201 . . . . . . . . . . . . . . . . 17  |-  ( H
" W )  =  ( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )
282273, 14syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
283 f1ofo 5681 . . . . . . . . . . . . . . . . . . 19  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  H : ( 1 ... M ) -onto-> ran  H
)
284282, 283syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -onto-> ran  H
)
28547ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
286 foimacnv 5692 . . . . . . . . . . . . . . . . . 18  |-  ( ( H : ( 1 ... M ) -onto-> ran 
H  /\  ( `' F " ( _V  \  {  .0.  } ) ) 
C_  ran  H )  ->  ( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )  =  ( `' F " ( _V  \  {  .0.  } ) ) )
287284, 285, 286syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )  =  ( `' F " ( _V  \  {  .0.  } ) ) )
288281, 287syl5eq 2480 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H " W
)  =  ( `' F " ( _V 
\  {  .0.  }
) ) )
289 f1oeq3 5667 . . . . . . . . . . . . . . . 16  |-  ( ( H " W )  =  ( `' F " ( _V  \  {  .0.  } ) )  -> 
( ( H  |`  W ) : W -1-1-onto-> ( H " W )  <->  ( H  |`  W ) : W -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) ) )
290288, 289syl 16 . . . . . . . . . . . . . . 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.  }
) ) ) )
291276, 290mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
292 simprr 734 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 W ) ) ,  W ) )
293 isof1o 6045 . . . . . . . . . . . . . . 15  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 W ) ) ,  W )  -> 
f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )
294292, 293syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )
295 f1oco 5698 . . . . . . . . . . . . . 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.  }
) ) )
296291, 294, 295syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( H  |`  W )  o.  f
) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
297 f1of 5674 . . . . . . . . . . . . . . . . 17  |-  ( f : ( 1 ... ( # `  W
) ) -1-1-onto-> W  ->  f :
( 1 ... ( # `
 W ) ) --> W )
298294, 297syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f : ( 1 ... ( # `  W
) ) --> W )
299 frn 5597 . . . . . . . . . . . . . . . 16  |-  ( f : ( 1 ... ( # `  W
) ) --> W  ->  ran  f  C_  W )
300298, 299syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  f  C_  W )
301 cores 5373 . . . . . . . . . . . . . . 15  |-  ( ran  f  C_  W  ->  ( ( H  |`  W )  o.  f )  =  ( H  o.  f
) )
302300, 301syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( H  |`  W )  o.  f
)  =  ( H  o.  f ) )
303 f1oeq1 5665 . . . . . . . . . . . . . 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.  }
) ) ) )
304302, 303syl 16 . . . . . . . . . . . . 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.  }
) ) ) )
305296, 304mpbid 202 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
306 resexg 5185 . . . . . . . . . . . . . . . . . 18  |-  ( H  e.  _V  ->  ( H  |`  W )  e. 
_V )
307126, 306syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( H  |`  W )  e.  _V )
308307ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W )  e.  _V )
309 f1oen3g 7123 . . . . . . . . . . . . . . . 16  |-  ( ( ( H  |`  W )  e.  _V  /\  ( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )  ->  W  ~~  ( `' F " ( _V 
\  {  .0.  }
) ) )
310308, 291, 309syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  ~~  ( `' F " ( _V  \  {  .0.  } ) ) )
311265ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  e.  Fin )
312 ssfi 7329 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  H  e.  Fin  /\  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )  ->  ( `' F " ( _V 
\  {  .0.  }
) )  e.  Fin )
313131, 47, 312syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  e. 
Fin )
314313ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  e. 
Fin )
315 hashen 11631 . . . . . . . . . . . . . . . 16  |-  ( ( W  e.  Fin  /\  ( `' F " ( _V 
\  {  .0.  }
) )  e.  Fin )  ->  ( ( # `  W )  =  (
# `  ( `' F " ( _V  \  {  .0.  } ) ) )  <->  W  ~~  ( `' F " ( _V 
\  {  .0.  }
) ) ) )
316311, 314, 315syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( # `  W
)  =  ( # `  ( `' F "
( _V  \  {  .0.  } ) ) )  <-> 
W  ~~  ( `' F " ( _V  \  {  .0.  } ) ) ) )
317310, 316mpbird 224 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( # `  W )  =  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) )
318317oveq2d 6097 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( 1 ... ( # `
 W ) )  =  ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )
319 f1oeq2 5666 . . . . . . . . . . . . 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.  } ) ) ) )
320318, 319syl 16 . . . . . . . . . . . 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.  } ) ) ) )
321305, 320mpbid 202 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
) : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) )
322317fveq2d 5732 . . . . . . . . . . 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.  }
) ) ) ) )
323321, 322jca 519 . . . . . . . . . 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.  } ) ) ) ) ) )
324 f1oeq1 5665 . . . . . . . . . . . 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.  } ) ) ) )
325 coeq2 5031 . . . . . . . . . . . . . . 15  |-  ( g  =  ( H  o.  f )  ->  ( F  o.  g )  =  ( F  o.  ( H  o.  f
) ) )
326325seqeq3d 11331 . . . . . . . . . . . . . 14  |-  ( g  =  ( H  o.  f )  ->  seq  1 (  .+  , 
( F  o.  g
) )  =  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) )
327326fveq1d 5730 . . . . . . . . . . . . 13  |-  ( g  =  ( H  o.  f )  ->  (  seq  1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) )  =  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )
328327eqeq2d 2447 . . . . . . . . . . . 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.  }
) ) ) ) ) )
329324, 328anbi12d 692 . . . . . . . . . . 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.  }
) ) ) ) ) ) )
330329spcegv 3037 . . . . . . . . . 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.  } ) ) ) ) ) ) )
331272, 323, 330sylc 58 . . . . . . . . 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.  } ) ) ) ) ) )
3321ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  G  e.  Mnd )
3332ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  A  e.  V )
3347ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  F : A --> B )
335148ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
336 imaeq2 5199 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )  =  ( `' H "
(/) ) )
337 ima0 5221 . . . . . . . . . . . . . . . . . 18  |-  ( `' H " (/) )  =  (/)
338336, 337syl6eq 2484 . . . . . . . . . . . . . . . . 17  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )  =  (/) )
339280, 338syl5eq 2480 . . . . . . . . . . . . . . . 16  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  W  =  (/) )
340339necon3i 2643 . . . . . . . . . . . . . . 15  |-  ( W  =/=  (/)  ->  ( `' F " ( _V  \  {  .0.  } ) )  =/=  (/) )
341340ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  =/=  (/) )
342111ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  H  C_  A )
343285, 342sstrd 3358 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  C_  A )
34458, 3, 61, 151, 332, 333, 334, 335, 314, 341, 343gsumval3eu 15513 . . . . . . . . . . . . 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.  }
) ) ) ) ) )
345 iota1 5432 . . . . . . . . . . . . 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 ) )
346344, 345syl 16 . . . . . . . . . . . 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 ) )
347 eqid 2436 . . . . . . . . . . . . . 14  |-  ( `' F " ( _V 
\  {  .0.  }
) )  =  ( `' F " ( _V 
\  {  .0.  }
) )
348 simprl 733 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  -.  A  e.  ran  ... )
34958, 3, 61, 151, 332, 333, 334, 335, 314, 341, 347, 348gsumval3a 15512 . . . . . . . . . . . . 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.  } ) ) ) ) ) ) )
350349eqeq1d 2444 . . . . . . . . . . . 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 ) )
351346, 350bitr4d 248 . . . . . . . . . . 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 ) )
352351alrimiv 1641 . . . . . . . . . 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 ) )
353 fvex 5742 . . . . . . . . . . 11  |-  (  seq  1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) )  e.  _V
354 eqeq1 2442 . . . . . . . . . . . . . 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.  }
) ) ) ) ) )
355354anbi2d 685 . . . . . . . . . . . . 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.  }
) ) ) ) ) ) )
356355exbidv 1636 . . . . . . . . . . . 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.  } ) ) ) ) ) ) )
357 eqeq2 2445 . . . . . . . . . . . 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 ) ) ) )
358356, 357bibi12d 313 . . . . . . . . . . 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 ) ) ) ) )
359353, 358spcv 3042 . . . . . . . . . 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 ) ) ) )
360352, 359syl 16 . . . . . . . . 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
) ) ) )
361331, 360mpbid 202 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( G  gsumg  F )  =  (  seq  1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) ) )
362332, 210sylan 458 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
363332, 212sylan 458 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
364332, 146sylan 458 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
365332, 59syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  .0.  e.  B )
366 simplr 732 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  =/=  (/) )
36731ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( F  o.  H
) : ( 1 ... M ) --> B )
368367ffvelrnda 5870 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  x )  e.  B
)
36934a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )  C_  W )
370367, 369suppssr 5864 . . . . . . . . 9  |-  (