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

Theorem gsumval3OLD 16385
Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) Obsolete version of gsumval3 16388 as of 31-May-2019. (New usage is discouraged.) (Proof modification is discouraged.)
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 ) )
gsumval3OLD.m  |-  ( ph  ->  M  e.  NN )
gsumval3OLD.h  |-  ( ph  ->  H : ( 1 ... M ) -1-1-> A
)
gsumval3OLD.n  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
gsumval3OLD.w  |-  W  =  ( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )
Assertion
Ref Expression
gsumval3OLD  |-  ( ph  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )

Proof of Theorem gsumval3OLD
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 15514 . . . . 5  |-  ( ( G  e.  Mnd  /\  A  e.  V )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
51, 2, 4syl2anc 661 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
65adantr 465 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
7 gsumval3.f . . . . . . 7  |-  ( ph  ->  F : A --> B )
87feqmptd 5747 . . . . . 6  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
98adantr 465 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
10 gsumval3OLD.h . . . . . . . . . . . . . 14  |-  ( ph  ->  H : ( 1 ... M ) -1-1-> A
)
11 f1f 5609 . . . . . . . . . . . . . 14  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) --> A )
1210, 11syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  H : ( 1 ... M ) --> A )
1312ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  ->  H : ( 1 ... M ) --> A )
14 f1f1orn 5655 . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  H :
( 1 ... M
)
-1-1-onto-> ran  H )
17 f1ocnv 5656 . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . 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 5846 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( 1 ... M ) )
22 fvco3 5771 . . . . . . . . . . . 12  |-  ( ( H : ( 1 ... M ) --> A  /\  ( `' H `  x )  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `  ( H `  ( `' H `  x )
) ) )
2313, 21, 22syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `
 ( H `  ( `' H `  x ) ) ) )
24 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  W  =  (/) )  ->  W  =  (/) )
2524difeq2d 3477 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( ( 1 ... M
)  \  (/) ) )
26 dif0 3752 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M ) 
\  (/) )  =  ( 1 ... M )
2725, 26syl6eq 2491 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( 1 ... M ) )
2827adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( 1 ... M )  \  W
)  =  ( 1 ... M ) )
2921, 28eleqtrrd 2520 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( ( 1 ... M
)  \  W )
)
30 fco 5571 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> B  /\  H : ( 1 ... M ) --> A )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
317, 12, 30syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  o.  H
) : ( 1 ... M ) --> B )
3231adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
33 gsumval3OLD.w . . . . . . . . . . . . . . 15  |-  W  =  ( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )
3433eqimss2i 3414 . . . . . . . . . . . . . 14  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  W
3534a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  W
)
3632, 35suppssrOLD 5840 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  ( `' H `  x )  e.  ( ( 1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
3729, 36syldan 470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
38 f1ocnvfv2 5987 . . . . . . . . . . . . 13  |-  ( ( H : ( 1 ... M ) -1-1-onto-> ran  H  /\  x  e.  ran  H )  ->  ( H `  ( `' H `  x ) )  =  x )
3916, 38sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( H `  ( `' H `  x ) )  =  x )
4039fveq2d 5698 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  ( H `  ( `' H `  x )
) )  =  ( F `  x ) )
4123, 37, 403eqtr3rd 2484 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  =  .0.  )
42 fvex 5704 . . . . . . . . . . 11  |-  ( F `
 x )  e. 
_V
4342elsnc 3904 . . . . . . . . . 10  |-  ( ( F `  x )  e.  {  .0.  }  <->  ( F `  x )  =  .0.  )
4441, 43sylibr 212 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  e.  {  .0.  } )
4544adantlr 714 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
46 eldif 3341 . . . . . . . . . . 11  |-  ( x  e.  ( A  \  ran  H )  <->  ( x  e.  A  /\  -.  x  e.  ran  H ) )
47 gsumval3OLD.n . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
487, 47suppssrOLD 5840 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  =  .0.  )
4948, 43sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  e.  {  .0.  } )
5046, 49sylan2br 476 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5150adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5251anassrs 648 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  -.  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
5345, 52pm2.61dan 789 . . . . . . 7  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  e.  {  .0.  } )
5453, 43sylib 196 . . . . . 6  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  =  .0.  )
5554mpteq2dva 4381 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  .0.  ) )
569, 55eqtrd 2475 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  .0.  ) )
5756oveq2d 6110 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  ( G 
gsumg  ( x  e.  A  |->  .0.  ) ) )
58 gsumval3.b . . . . . . . 8  |-  B  =  ( Base `  G
)
5958, 3mndidcl 15442 . . . . . . 7  |-  ( G  e.  Mnd  ->  .0.  e.  B )
601, 59syl 16 . . . . . 6  |-  ( ph  ->  .0.  e.  B )
61 gsumval3.p . . . . . . 7  |-  .+  =  ( +g  `  G )
6258, 61, 3mndlid 15444 . . . . . 6  |-  ( ( G  e.  Mnd  /\  .0.  e.  B )  -> 
(  .0.  .+  .0.  )  =  .0.  )
631, 60, 62syl2anc 661 . . . . 5  |-  ( ph  ->  (  .0.  .+  .0.  )  =  .0.  )
6463adantr 465 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  (  .0.  .+  .0.  )  =  .0.  )
65 gsumval3OLD.m . . . . . 6  |-  ( ph  ->  M  e.  NN )
66 nnuz 10899 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
6765, 66syl6eleq 2533 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
6867adantr 465 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  M  e.  ( ZZ>= `  1 )
)
6927eleq2d 2510 . . . . . 6  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  ( ( 1 ... M )  \  W
)  <->  x  e.  (
1 ... M ) ) )
7069biimpar 485 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  x  e.  ( ( 1 ... M )  \  W
) )
7132, 35suppssrOLD 5840 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( ( 1 ... M )  \  W
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7270, 71syldan 470 . . . 4  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7364, 68, 72seqid3 11853 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
)  =  .0.  )
746, 57, 733eqtr4d 2485 . 2  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
) )
75 fzf 11444 . . . . 5  |-  ... :
( ZZ  X.  ZZ )
--> ~P ZZ
76 ffn 5562 . . . . 5  |-  ( ...
: ( ZZ  X.  ZZ ) --> ~P ZZ  ->  ... 
Fn  ( ZZ  X.  ZZ ) )
77 ovelrn 6242 . . . . 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 725 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  G  e.  Mnd )
80 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =  ( m ... n ) )
81 frel 5565 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  Rel  F )
827, 81syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Rel  F )
83 reldm0 5060 . . . . . . . . . . . . . . . . 17  |-  ( Rel 
F  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
8482, 83syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
85 fdm 5566 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  dom  F  =  A )
867, 85syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  A )
8786eqeq1d 2451 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( dom  F  =  (/) 
<->  A  =  (/) ) )
8884, 87bitrd 253 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F  =  (/)  <->  A  =  (/) ) )
89 coeq1 5000 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  =  (/)  ->  ( F  o.  H )  =  ( (/)  o.  H
) )
90 co01 5355 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  o.  H )  =  (/)
9189, 90syl6eq 2491 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  =  (/)  ->  ( F  o.  H )  =  (/) )
9291cnveqd 5018 . . . . . . . . . . . . . . . . . . 19  |-  ( F  =  (/)  ->  `' ( F  o.  H )  =  `' (/) )
93 cnv0 5243 . . . . . . . . . . . . . . . . . . 19  |-  `' (/)  =  (/)
9492, 93syl6eq 2491 . . . . . . . . . . . . . . . . . 18  |-  ( F  =  (/)  ->  `' ( F  o.  H )  =  (/) )
9594imaeq1d 5171 . . . . . . . . . . . . . . . . 17  |-  ( F  =  (/)  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  (
(/) " ( _V  \  {  .0.  } ) ) )
96 0ima 5188 . . . . . . . . . . . . . . . . 17  |-  ( (/) " ( _V  \  {  .0.  } ) )  =  (/)
9795, 96syl6eq 2491 . . . . . . . . . . . . . . . 16  |-  ( F  =  (/)  ->  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  (/) )
9833, 97syl5eq 2487 . . . . . . . . . . . . . . 15  |-  ( F  =  (/)  ->  W  =  (/) )
9988, 98syl6bir 229 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  =  (/)  ->  W  =  (/) ) )
10099necon3d 2649 . . . . . . . . . . . . 13  |-  ( ph  ->  ( W  =/=  (/)  ->  A  =/=  (/) ) )
101100imp 429 . . . . . . . . . . . 12  |-  ( (
ph  /\  W  =/=  (/) )  ->  A  =/=  (/) )
102101adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =/=  (/) )
10380, 102eqnetrrd 2631 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( m ... n
)  =/=  (/) )
104 fzn0 11467 . . . . . . . . . 10  |-  ( ( m ... n )  =/=  (/)  <->  n  e.  ( ZZ>=
`  m ) )
105103, 104sylib 196 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  n  e.  ( ZZ>= `  m ) )
1067ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : A --> B )
10780feq2d 5550 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( F : A --> B 
<->  F : ( m ... n ) --> B ) )
108106, 107mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : ( m ... n ) --> B )
10958, 61, 79, 105, 108gsumval2 15516 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq m (  .+  ,  F ) `  n
) )
110 frn 5568 . . . . . . . . . . . . . . 15  |-  ( H : ( 1 ... M ) --> A  ->  ran  H  C_  A )
11112, 110syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  C_  A
)
112111ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  A )
113112, 80sseqtrd 3395 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  ( m ... n ) )
114 fzssuz 11502 . . . . . . . . . . . . 13  |-  ( m ... n )  C_  ( ZZ>= `  m )
115 uzssz 10883 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  m )  C_  ZZ
116 zssre 10656 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
117115, 116sstri 3368 . . . . . . . . . . . . 13  |-  ( ZZ>= `  m )  C_  RR
118114, 117sstri 3368 . . . . . . . . . . . 12  |-  ( m ... n )  C_  RR
119113, 118syl6ss 3371 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  RR )
120 ltso 9458 . . . . . . . . . . 11  |-  <  Or  RR
121 soss 4662 . . . . . . . . . . 11  |-  ( ran 
H  C_  RR  ->  (  <  Or  RR  ->  < 
Or  ran  H )
)
122119, 120, 121mpisyl 18 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  <  Or  ran  H )
123 fzfi 11797 . . . . . . . . . . . 12  |-  ( 1 ... M )  e. 
Fin
124123a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
125 fex2 6535 . . . . . . . . . . . . . . 15  |-  ( ( H : ( 1 ... M ) --> A  /\  ( 1 ... M )  e.  Fin  /\  A  e.  V )  ->  H  e.  _V )
12612, 124, 2, 125syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( ph  ->  H  e.  _V )
127 f1oen3g 7328 . . . . . . . . . . . . . 14  |-  ( ( H  e.  _V  /\  H : ( 1 ... M ) -1-1-onto-> ran  H )  -> 
( 1 ... M
)  ~~  ran  H )
128126, 15, 127syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  ~~  ran  H )
129 enfi 7532 . . . . . . . . . . . . 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 211 . . . . . . . . . . 11  |-  ( ph  ->  ran  H  e.  Fin )
132131ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  e.  Fin )
133 fz1iso 12218 . . . . . . . . . 10  |-  ( (  <  Or  ran  H  /\  ran  H  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
134122, 132, 133syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
13565nnnn0d 10639 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  NN0 )
136 hashfz1 12120 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN0  ->  ( # `  ( 1 ... M
) )  =  M )
137135, 136syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  M )
138 hashen 12121 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ran  H  e.  Fin )  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
139123, 131, 138sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
140128, 139mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  ( # `  ran  H ) )
141137, 140eqtr3d 2477 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  =  ( # `  ran  H ) )
142141ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  =  ( # `  ran  H ) )
143142fveq2d 5698 . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  G  e.  Mnd )
14558, 61mndcl 15423 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  Mnd  /\  x  e.  B  /\  y  e.  B )  ->  ( x  .+  y
)  e.  B )
1461453expb 1188 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
147144, 146sylan 471 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
150149sselda 3359 . . . . . . . . . . . . . . 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 15850 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( Z `
 ran  F )  /\  y  e.  ran  F )  ->  ( x  .+  y )  =  ( y  .+  x ) )
153150, 152sylan 471 . . . . . . . . . . . . . 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 647 . . . . . . . . . . . . 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 15424 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B
) )  ->  (
( x  .+  y
)  .+  z )  =  ( x  .+  ( y  .+  z
) ) )
156144, 155sylan 471 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  e.  ( ZZ>= ` 
1 ) )
1587ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> B )
159 frn 5568 . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 ran  H )
) ,  ran  H
) )
162 isof1o 6019 . . . . . . . . . . . . . . . . 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 6110 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( 1 ... M
)  =  ( 1 ... ( # `  ran  H ) ) )
165 f1oeq2 5636 . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) -1-1-onto-> ran  H
)
168 f1ocnv 5656 . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
171 f1oco 5666 . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . 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 5562 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  F  Fn  A )
174 dffn4 5629 . . . . . . . . . . . . . . . . . 18  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
175173, 174sylib 196 . . . . . . . . . . . . . . . . 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 5623 . . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  A )
182 fss 5570 . . . . . . . . . . . . . . . 16  |-  ( ( f : ( 1 ... M ) --> ran 
H  /\  ran  H  C_  A )  ->  f : ( 1 ... M ) --> A )
183180, 181, 182syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> A )
184 fco 5571 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> ran  F  /\  f : ( 1 ... M ) --> A )  ->  ( F  o.  f ) : ( 1 ... M ) --> ran  F )
185178, 183, 184syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  f
) : ( 1 ... M ) --> ran 
F )
186185ffvelrnda 5846 . . . . . . . . . . . . 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 5670 . . . . . . . . . . . . . . . . . . . . . 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 5004 . . . . . . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . . . . . . . . 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 5589 . . . . . . . . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( (
f  o.  `' f )  o.  H ) )
195 coass 5359 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  o.  `' f )  o.  H )  =  ( f  o.  ( `' f  o.  H ) )
196194, 195syl6eq 2491 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( f  o.  ( `' f  o.  H ) ) )
197196coeq2d 5005 . . . . . . . . . . . . . . . . 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 5359 . . . . . . . . . . . . . . . . 17  |-  ( ( F  o.  f )  o.  ( `' f  o.  H ) )  =  ( F  o.  ( f  o.  ( `' f  o.  H
) ) )
199197, 198syl6eqr 2493 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( ( F  o.  f )  o.  ( `' f  o.  H ) ) )
200199fveq1d 5696 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . . . 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 5571 . . . . . . . . . . . . . . . 16  |-  ( ( `' f : ran  H --> ( 1 ... M
)  /\  H :
( 1 ... M
) --> ran  H )  ->  ( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
205203, 191, 204syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
206 fvco3 5771 . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . 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 11850 . . . . . . . . . . . 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 15444 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
211144, 210sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
21258, 61, 3mndrid 15445 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
213144, 212sylan 471 . . . . . . . . . . . . 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 5566 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) --> A  ->  dom  H  =  ( 1 ... M ) )
21612, 215syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  H  =  ( 1 ... M ) )
217 eluzfz1 11461 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
21867, 217syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ( 1 ... M ) )
219 ne0i 3646 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
220218, 219syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
221216, 220eqnetrd 2629 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  H  =/=  (/) )
222 dm0rn0 5059 . . . . . . . . . . . . . . . 16  |-  ( dom 
H  =  (/)  <->  ran  H  =  (/) )
223222necon3bii 2643 . . . . . . . . . . . . . . 15  |-  ( dom 
H  =/=  (/)  <->  ran  H  =/=  (/) )
224221, 223sylib 196 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  =/=  (/) )
225224ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  =/=  (/) )
226113adantrr 716 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  ( m ... n ) )
227 simprl 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  A  =  ( m ... n ) )
228227eleq2d 2510 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  A  <->  x  e.  ( m ... n ) ) )
229228biimpar 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  ->  x  e.  A )
230158ffvelrnda 5846 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
231229, 230syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  -> 
( F `  x
)  e.  B )
232227difeq1d 3476 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( A  \  ran  H )  =  ( ( m ... n ) 
\  ran  H )
)
233232eleq2d 2510 . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ph )
236235, 48sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( A  \  ran  H ) )  ->  ( F `  x )  =  .0.  )
237234, 236syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  -> 
( F `  x
)  =  .0.  )
238 f1of 5644 . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . 14  |-  ( ( f : ( 1 ... ( # `  ran  H ) ) --> ran  H  /\  y  e.  (
1 ... ( # `  ran  H ) ) )  -> 
( ( F  o.  f ) `  y
)  =  ( F `
 ( f `  y ) ) )
241239, 240sylan 471 . . . . . . . . . . . . 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 12220 . . . . . . . . . . . 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 2485 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq 1 (  .+  ,  ( F  o.  H ) ) `  M )  =  (  seq m (  .+  ,  F ) `  n
) )
244243expr 615 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H )  ->  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
)  =  (  seq m (  .+  ,  F ) `  n
) ) )
245244exlimdv 1690 . . . . . . . . 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 2478 . . . . . . 7  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )
248247ex 434 . . . . . 6  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
249248rexlimdvw 2847 . . . . 5  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
250249rexlimdvw 2847 . . . 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 217 . . 3  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  e.  ran  ...  ->  ( G 
gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
252 cnvimass 5192 . . . . . . . . . . 11  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  C_  dom  ( F  o.  H
)
25333, 252eqsstri 3389 . . . . . . . . . 10  |-  W  C_  dom  ( F  o.  H
)
254 fdm 5566 . . . . . . . . . . 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 3407 . . . . . . . . 9  |-  ( ph  ->  W  C_  ( 1 ... M ) )
257 fzssuz 11502 . . . . . . . . . . 11  |-  ( 1 ... M )  C_  ( ZZ>= `  1 )
258257, 66sseqtr4i 3392 . . . . . . . . . 10  |-  ( 1 ... M )  C_  NN
259 nnssre 10329 . . . . . . . . . 10  |-  NN  C_  RR
260258, 259sstri 3368 . . . . . . . . 9  |-  ( 1 ... M )  C_  RR
261256, 260syl6ss 3371 . . . . . . . 8  |-  ( ph  ->  W  C_  RR )
262 soss 4662 . . . . . . . 8  |-  ( W 
C_  RR  ->  (  < 
Or  RR  ->  <  Or  W ) )
263261, 120, 262mpisyl 18 . . . . . . 7  |-  ( ph  ->  <  Or  W )
264 ssfi 7536 . . . . . . . 8  |-  ( ( ( 1 ... M
)  e.  Fin  /\  W  C_  ( 1 ... M ) )  ->  W  e.  Fin )
265123, 256, 264sylancr 663 . . . . . . 7  |-  ( ph  ->  W  e.  Fin )
266 fz1iso 12218 . . . . . . 7  |-  ( (  <  Or  W  /\  W  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
267263, 265, 266syl2anc 661 . . . . . 6  |-  ( ph  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
268267ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
269 vex 2978 . . . . . . . . . . . 12  |-  f  e. 
_V
270 coexg 6531 . . . . . . . . . . . 12  |-  ( ( H  e.  _V  /\  f  e.  _V )  ->  ( H  o.  f
)  e.  _V )
271126, 269, 270sylancl 662 . . . . . . . . . . 11  |-  ( ph  ->  ( H  o.  f
)  e.  _V )
272271ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
)  e.  _V )
27310ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  H : ( 1 ... M ) -1-1-> A )
274256ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  C_  ( 1 ... M ) )
275 f1ores 5658 . . . . . . . . . . . . . . . 16  |-  ( ( H : ( 1 ... M ) -1-1-> A  /\  W  C_  ( 1 ... M ) )  ->  ( H  |`  W ) : W -1-1-onto-> ( H " W ) )
276273, 274, 275syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W ) : W -1-1-onto-> ( H " W
) )
277 cnvco 5028 . . . . . . . . . . . . . . . . . . . 20  |-  `' ( F  o.  H )  =  ( `' H  o.  `' F )
278277imaeq1i 5169 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( F  o.  H
) " ( _V 
\  {  .0.  }
) )  =  ( ( `' H  o.  `' F ) " ( _V  \  {  .0.  }
) )
279 imaco 5346 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' H  o.  `' F ) " ( _V  \  {  .0.  }
) )  =  ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) )
28033, 278, 2793eqtri 2467 . . . . . . . . . . . . . . . . . 18  |-  W  =  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )
281280imaeq2i 5170 . . . . . . . . . . . . . . . . 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 5651 . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )
286 foimacnv 5661 . . . . . . . . . . . . . . . . . 18  |-  ( ( H : ( 1 ... M ) -onto-> ran 
H  /\  ( `' F " ( _V  \  {  .0.  } ) ) 
C_  ran  H )  ->  ( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )  =  ( `' F " ( _V  \  {  .0.  } ) ) )
287284, 285, 286syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H " ( `' H " ( `' F " ( _V 
\  {  .0.  }
) ) ) )  =  ( `' F " ( _V  \  {  .0.  } ) ) )
288281, 287syl5eq 2487 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H " W
)  =  ( `' F " ( _V 
\  {  .0.  }
) ) )
289 f1oeq3 5637 . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
292 simprr 756 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 W ) ) ,  W ) )
293 isof1o 6019 . . . . . . . . . . . . . . 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 5666 . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... ( # `  W
) ) -1-1-onto-> W  ->  f :
( 1 ... ( # `
 W ) ) --> W )
298294, 297syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f : ( 1 ... ( # `  W
) ) --> W )
299 frn 5568 . . . . . . . . . . . . . 14  |-  ( f : ( 1 ... ( # `  W
) ) --> W  ->  ran  f  C_  W )
300 cores 5344 . . . . . . . . . . . . . 14  |-  ( ran  f  C_  W  ->  ( ( H  |`  W )  o.  f )  =  ( H  o.  f
) )
301 f1oeq1 5635 . . . . . . . . . . . . . 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.  }
) ) ) )
302298, 299, 300, 3014syl 21 . . . . . . . . . . . . 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.  }
) ) ) )
303296, 302mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
) : ( 1 ... ( # `  W
) ) -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )
304 resexg 5152 . . . . . . . . . . . . . . . . . 18  |-  ( H  e.  _V  ->  ( H  |`  W )  e. 
_V )
305126, 304syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( H  |`  W )  e.  _V )
306305ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  |`  W )  e.  _V )
307 f1oen3g 7328 . . . . . . . . . . . . . . . 16  |-  ( ( ( H  |`  W )  e.  _V  /\  ( H  |`  W ) : W -1-1-onto-> ( `' F "
( _V  \  {  .0.  } ) ) )  ->  W  ~~  ( `' F " ( _V 
\  {  .0.  }
) ) )
308306, 291, 307syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  ~~  ( `' F " ( _V  \  {  .0.  } ) ) )
309265ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  e.  Fin )
310 ssfi 7536 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  H  e.  Fin  /\  ( `' F "
( _V  \  {  .0.  } ) )  C_  ran  H )  ->  ( `' F " ( _V 
\  {  .0.  }
) )  e.  Fin )
311131, 47, 310syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' F "
( _V  \  {  .0.  } ) )  e. 
Fin )
312311ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  e. 
Fin )
313 hashen 12121 . . . . . . . . . . . . . . . 16  |-  ( ( W  e.  Fin  /\  ( `' F " ( _V 
\  {  .0.  }
) )  e.  Fin )  ->  ( ( # `  W )  =  (
# `  ( `' F " ( _V  \  {  .0.  } ) ) )  <->  W  ~~  ( `' F " ( _V 
\  {  .0.  }
) ) ) )
314309, 312, 313syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( # `  W
)  =  ( # `  ( `' F "
( _V  \  {  .0.  } ) ) )  <-> 
W  ~~  ( `' F " ( _V  \  {  .0.  } ) ) ) )
315308, 314mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( # `  W )  =  ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) )
316315oveq2d 6110 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( 1 ... ( # `
 W ) )  =  ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) )
317 f1oeq2 5636 . . . . . . . . . . . . 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.  } ) ) ) )
318316, 317syl 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.  } ) ) ) )
319303, 318mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( H  o.  f
) : ( 1 ... ( # `  ( `' F " ( _V 
\  {  .0.  }
) ) ) ) -1-1-onto-> ( `' F " ( _V 
\  {  .0.  }
) ) )
320315fveq2d 5698 . . . . . . . . . . 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.  } ) ) ) ) )
321319, 320jca 532 . . . . . . . . . 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.  } ) ) ) ) ) )
322 f1oeq1 5635 . . . . . . . . . . . 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.  } ) ) ) )
323 coeq2 5001 . . . . . . . . . . . . . . 15  |-  ( g  =  ( H  o.  f )  ->  ( F  o.  g )  =  ( F  o.  ( H  o.  f
) ) )
324323seqeq3d 11817 . . . . . . . . . . . . . 14  |-  ( g  =  ( H  o.  f )  ->  seq 1 (  .+  , 
( F  o.  g
) )  =  seq 1 (  .+  , 
( F  o.  ( H  o.  f )
) ) )
325324fveq1d 5696 . . . . . . . . . . . . 13  |-  ( g  =  ( H  o.  f )  ->  (  seq 1 (  .+  , 
( F  o.  g
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) )  =  (  seq 1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 ( `' F " ( _V  \  {  .0.  } ) ) ) ) )
326325eqeq2d 2454 . . . . . . . . . . . 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.  }
) ) ) ) ) )
327322, 326anbi12d 710 . . . . . . . . . . 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.  }
) ) ) ) ) ) )
328327spcegv 3061 . . . . . . . . . 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.  } ) ) ) ) ) ) )
329272, 321, 328sylc 60 . . . . . . . . 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.  } ) ) ) ) ) )
3301ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  G  e.  Mnd )
3312ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  A  e.  V )
3327ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  F : A --> B )
333148ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
334 imaeq2 5168 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )  =  ( `' H "
(/) ) )
335 ima0 5187 . . . . . . . . . . . . . . . . . 18  |-  ( `' H " (/) )  =  (/)
336334, 335syl6eq 2491 . . . . . . . . . . . . . . . . 17  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  ( `' H "
( `' F "
( _V  \  {  .0.  } ) ) )  =  (/) )
337280, 336syl5eq 2487 . . . . . . . . . . . . . . . 16  |-  ( ( `' F " ( _V 
\  {  .0.  }
) )  =  (/)  ->  W  =  (/) )
338337necon3i 2653 . . . . . . . . . . . . . . 15  |-  ( W  =/=  (/)  ->  ( `' F " ( _V  \  {  .0.  } ) )  =/=  (/) )
339338ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  =/=  (/) )
340111ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  ran  H  C_  A )
341285, 340sstrd 3369 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' F "
( _V  \  {  .0.  } ) )  C_  A )
34258, 3, 61, 151, 330, 331, 332, 333, 312, 339, 341gsumval3eu 16384 . . . . . . . . . . . . 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.  }
) ) ) ) ) )
343 iota1 5398 . . . . . . . . . . . . 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 ) )
344342, 343syl 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 ) )
345 eqid 2443 . . . . . . . . . . . . . 14  |-  ( `' F " ( _V 
\  {  .0.  }
) )  =  ( `' F " ( _V 
\  {  .0.  }
) )
346 simprl 755 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  -.  A  e.  ran  ... )
34758, 3, 61, 151, 330, 331, 332, 333, 312, 339, 345, 346gsumval3aOLD 16383 . . . . . . . . . . . . 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.  } ) ) ) ) ) ) )
348347eqeq1d 2451 . . . . . . . . . . . 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 ) )
349344, 348bitr4d 256 . . . . . . . . . . 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 ) )
350349alrimiv 1685 . . . . . . . . . 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 ) )
351 fvex 5704 . . . . . . . . . . 11  |-  (  seq 1 (  .+  , 
( F  o.  ( H  o.  f )
) ) `  ( # `
 W ) )  e.  _V
352 eqeq1 2449 . . . . . . . . . . . . . 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.  }
) ) ) ) ) )
353352anbi2d 703 . . . . . . . . . . . . 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.  }
) ) ) ) ) ) )
354353exbidv 1680 . . . . . . . . . . . 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.  } ) ) ) ) ) ) )
355 eqeq2 2452 . . . . . . . . . . . 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 ) ) ) )
356354, 355bibi12d 321 . . . . . . . . . . 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 ) ) ) ) )
357351, 356spcv 3066 . . . . . . . . . 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 ) ) ) )
358350, 357syl 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
) ) ) )
359329, 358mpbid 210 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) ) )
360330, 210sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
361330, 212sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
362330, 146sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
363330, 59syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  .0.  e.  B )
364 simplr 754 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  =/=  (/) )
36531ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( F  o.  H
) : ( 1 ... M ) --> B )
366365ffvelrnda 5846 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  x )  e.  B
)
36734a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( `' ( F  o.  H ) "
( _V  \  {  .0.  } ) )  C_  W )
368365, 367suppssrOLD 5840 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  ( (
1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  x
)  =  .0.  )
369 coass 5359 . . . . . . . . . . 11  |-  ( ( F  o.  H )  o.  f )  =  ( F  o.  ( H  o.  f )
)
370369fveq1i 5695 . . . . . . . . . 10  |-  ( ( ( F  o.  H
)  o.  f ) `
 y )  =