ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seqf1og Unicode version

Theorem seqf1og 10582
Description: Rearrange a sum via an arbitrary bijection on  ( M ... N
). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 29-Aug-2025.)
Hypotheses
Ref Expression
seqf1o.1  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
seqf1o.2  |-  ( (
ph  /\  ( x  e.  C  /\  y  e.  C ) )  -> 
( x  .+  y
)  =  ( y 
.+  x ) )
seqf1o.3  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  -> 
( ( x  .+  y )  .+  z
)  =  ( x 
.+  ( y  .+  z ) ) )
seqf1o.4  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
seqf1o.5  |-  ( ph  ->  C  C_  S )
seqf1og.p  |-  ( ph  ->  .+  e.  V )
seqf1o.6  |-  ( ph  ->  F : ( M ... N ) -1-1-onto-> ( M ... N ) )
seqf1o.7  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( G `  x )  e.  C
)
seqf1o.8  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( H `  k )  =  ( G `  ( F `
 k ) ) )
seqf1og.g  |-  ( ph  ->  G  e.  W )
seqf1og.h  |-  ( ph  ->  H  e.  X )
Assertion
Ref Expression
seqf1og  |-  ( ph  ->  (  seq M ( 
.+  ,  H ) `
 N )  =  (  seq M ( 
.+  ,  G ) `
 N ) )
Distinct variable groups:    x, k, y, z, F    k, G, x, y, z    k, M, x, y, z    .+ , k, x, y, z    k, N, x, y, z    ph, k, x, y, z    S, k, x, y, z    C, k, x, y, z    k, H
Allowed substitution hints:    H( x, y, z)    V( x, y, z, k)    W( x, y, z, k)    X( x, y, z, k)

Proof of Theorem seqf1og
Dummy variables  f  g  s  t  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqf1o.6 . . 3  |-  ( ph  ->  F : ( M ... N ) -1-1-onto-> ( M ... N ) )
2 seqf1o.7 . . . 4  |-  ( (
ph  /\  x  e.  ( M ... N ) )  ->  ( G `  x )  e.  C
)
32fmpttd 5705 . . 3  |-  ( ph  ->  ( x  e.  ( M ... N ) 
|->  ( G `  x
) ) : ( M ... N ) --> C )
4 seqf1o.4 . . . . 5  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
5 oveq2 5918 . . . . . . . . . . 11  |-  ( x  =  M  ->  ( M ... x )  =  ( M ... M
) )
6 f1oeq23 5483 . . . . . . . . . . 11  |-  ( ( ( M ... x
)  =  ( M ... M )  /\  ( M ... x )  =  ( M ... M ) )  -> 
( f : ( M ... x ) -1-1-onto-> ( M ... x )  <-> 
f : ( M ... M ) -1-1-onto-> ( M ... M ) ) )
75, 5, 6syl2anc 411 . . . . . . . . . 10  |-  ( x  =  M  ->  (
f : ( M ... x ) -1-1-onto-> ( M ... x )  <->  f :
( M ... M
)
-1-1-onto-> ( M ... M ) ) )
85feq2d 5383 . . . . . . . . . 10  |-  ( x  =  M  ->  (
g : ( M ... x ) --> C  <-> 
g : ( M ... M ) --> C ) )
97, 8anbi12d 473 . . . . . . . . 9  |-  ( x  =  M  ->  (
( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  <->  ( f : ( M ... M ) -1-1-onto-> ( M ... M
)  /\  g :
( M ... M
) --> C ) ) )
10 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  M  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
( g  o.  f
) ) `  M
) )
11 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  M  ->  (  seq M (  .+  , 
g ) `  x
)  =  (  seq M (  .+  , 
g ) `  M
) )
1210, 11eqeq12d 2208 . . . . . . . . 9  |-  ( x  =  M  ->  (
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x )  <->  (  seq M (  .+  , 
( g  o.  f
) ) `  M
)  =  (  seq M (  .+  , 
g ) `  M
) ) )
139, 12imbi12d 234 . . . . . . . 8  |-  ( x  =  M  ->  (
( ( f : ( M ... x
)
-1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  ( (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  M )  =  (  seq M
(  .+  ,  g
) `  M )
) ) )
14132albidv 1878 . . . . . . 7  |-  ( x  =  M  ->  ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M
)  /\  g :
( M ... M
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  M )  =  (  seq M (  .+  ,  g ) `  M ) ) ) )
1514imbi2d 230 . . . . . 6  |-  ( x  =  M  ->  (
( ph  ->  A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x
)  /\  g :
( M ... x
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x ) ) )  <-> 
( ph  ->  A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M
)  /\  g :
( M ... M
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  M )  =  (  seq M (  .+  ,  g ) `  M ) ) ) ) )
16 oveq2 5918 . . . . . . . . . . 11  |-  ( x  =  k  ->  ( M ... x )  =  ( M ... k
) )
17 f1oeq23 5483 . . . . . . . . . . 11  |-  ( ( ( M ... x
)  =  ( M ... k )  /\  ( M ... x )  =  ( M ... k ) )  -> 
( f : ( M ... x ) -1-1-onto-> ( M ... x )  <-> 
f : ( M ... k ) -1-1-onto-> ( M ... k ) ) )
1816, 16, 17syl2anc 411 . . . . . . . . . 10  |-  ( x  =  k  ->  (
f : ( M ... x ) -1-1-onto-> ( M ... x )  <->  f :
( M ... k
)
-1-1-onto-> ( M ... k ) ) )
1916feq2d 5383 . . . . . . . . . 10  |-  ( x  =  k  ->  (
g : ( M ... x ) --> C  <-> 
g : ( M ... k ) --> C ) )
2018, 19anbi12d 473 . . . . . . . . 9  |-  ( x  =  k  ->  (
( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  <->  ( f : ( M ... k ) -1-1-onto-> ( M ... k
)  /\  g :
( M ... k
) --> C ) ) )
21 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  k  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
( g  o.  f
) ) `  k
) )
22 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  k  ->  (  seq M (  .+  , 
g ) `  x
)  =  (  seq M (  .+  , 
g ) `  k
) )
2321, 22eqeq12d 2208 . . . . . . . . 9  |-  ( x  =  k  ->  (
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x )  <->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )
2420, 23imbi12d 234 . . . . . . . 8  |-  ( x  =  k  ->  (
( ( f : ( M ... x
)
-1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  ( (
f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  k )  =  (  seq M
(  .+  ,  g
) `  k )
) ) )
25242albidv 1878 . . . . . . 7  |-  ( x  =  k  ->  ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k
)  /\  g :
( M ... k
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  k )  =  (  seq M (  .+  ,  g ) `  k ) ) ) )
2625imbi2d 230 . . . . . 6  |-  ( x  =  k  ->  (
( ph  ->  A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x
)  /\  g :
( M ... x
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x ) ) )  <-> 
( ph  ->  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k
)  /\  g :
( M ... k
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  k )  =  (  seq M (  .+  ,  g ) `  k ) ) ) ) )
27 oveq2 5918 . . . . . . . . . . 11  |-  ( x  =  ( k  +  1 )  ->  ( M ... x )  =  ( M ... (
k  +  1 ) ) )
28 f1oeq23 5483 . . . . . . . . . . 11  |-  ( ( ( M ... x
)  =  ( M ... ( k  +  1 ) )  /\  ( M ... x )  =  ( M ... ( k  +  1 ) ) )  -> 
( f : ( M ... x ) -1-1-onto-> ( M ... x )  <-> 
f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) ) ) )
2927, 27, 28syl2anc 411 . . . . . . . . . 10  |-  ( x  =  ( k  +  1 )  ->  (
f : ( M ... x ) -1-1-onto-> ( M ... x )  <->  f :
( M ... (
k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) ) ) )
3027feq2d 5383 . . . . . . . . . 10  |-  ( x  =  ( k  +  1 )  ->  (
g : ( M ... x ) --> C  <-> 
g : ( M ... ( k  +  1 ) ) --> C ) )
3129, 30anbi12d 473 . . . . . . . . 9  |-  ( x  =  ( k  +  1 )  ->  (
( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  <->  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C ) ) )
32 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  ( k  +  1 )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
( g  o.  f
) ) `  (
k  +  1 ) ) )
33 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  ( k  +  1 )  ->  (  seq M (  .+  , 
g ) `  x
)  =  (  seq M (  .+  , 
g ) `  (
k  +  1 ) ) )
3432, 33eqeq12d 2208 . . . . . . . . 9  |-  ( x  =  ( k  +  1 )  ->  (
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x )  <->  (  seq M (  .+  , 
( g  o.  f
) ) `  (
k  +  1 ) )  =  (  seq M (  .+  , 
g ) `  (
k  +  1 ) ) ) )
3531, 34imbi12d 234 . . . . . . . 8  |-  ( x  =  ( k  +  1 )  ->  (
( ( f : ( M ... x
)
-1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  ( (
f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M
(  .+  ,  g
) `  ( k  +  1 ) ) ) ) )
36352albidv 1878 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  A. g A. f ( ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) ) ) )
3736imbi2d 230 . . . . . 6  |-  ( x  =  ( k  +  1 )  ->  (
( ph  ->  A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x
)  /\  g :
( M ... x
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x ) ) )  <-> 
( ph  ->  A. g A. f ( ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) ) ) ) )
38 oveq2 5918 . . . . . . . . . . 11  |-  ( x  =  N  ->  ( M ... x )  =  ( M ... N
) )
39 f1oeq23 5483 . . . . . . . . . . 11  |-  ( ( ( M ... x
)  =  ( M ... N )  /\  ( M ... x )  =  ( M ... N ) )  -> 
( f : ( M ... x ) -1-1-onto-> ( M ... x )  <-> 
f : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
4038, 38, 39syl2anc 411 . . . . . . . . . 10  |-  ( x  =  N  ->  (
f : ( M ... x ) -1-1-onto-> ( M ... x )  <->  f :
( M ... N
)
-1-1-onto-> ( M ... N ) ) )
4138feq2d 5383 . . . . . . . . . 10  |-  ( x  =  N  ->  (
g : ( M ... x ) --> C  <-> 
g : ( M ... N ) --> C ) )
4240, 41anbi12d 473 . . . . . . . . 9  |-  ( x  =  N  ->  (
( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  <->  ( f : ( M ... N ) -1-1-onto-> ( M ... N
)  /\  g :
( M ... N
) --> C ) ) )
43 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  N  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
( g  o.  f
) ) `  N
) )
44 fveq2 5546 . . . . . . . . . 10  |-  ( x  =  N  ->  (  seq M (  .+  , 
g ) `  x
)  =  (  seq M (  .+  , 
g ) `  N
) )
4543, 44eqeq12d 2208 . . . . . . . . 9  |-  ( x  =  N  ->  (
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x )  <->  (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
g ) `  N
) ) )
4642, 45imbi12d 234 . . . . . . . 8  |-  ( x  =  N  ->  (
( ( f : ( M ... x
)
-1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  ( (
f : ( M ... N ) -1-1-onto-> ( M ... N )  /\  g : ( M ... N ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  N )  =  (  seq M
(  .+  ,  g
) `  N )
) ) )
47462albidv 1878 . . . . . . 7  |-  ( x  =  N  ->  ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x )  /\  g : ( M ... x ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  x
)  =  (  seq M (  .+  , 
g ) `  x
) )  <->  A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N
)  /\  g :
( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  N )  =  (  seq M (  .+  ,  g ) `  N ) ) ) )
4847imbi2d 230 . . . . . 6  |-  ( x  =  N  ->  (
( ph  ->  A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x
)  /\  g :
( M ... x
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  x )  =  (  seq M (  .+  ,  g ) `  x ) ) )  <-> 
( ph  ->  A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N
)  /\  g :
( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  N )  =  (  seq M (  .+  ,  g ) `  N ) ) ) ) )
49 f1of 5492 . . . . . . . . . . . . . 14  |-  ( f : ( M ... M ) -1-1-onto-> ( M ... M
)  ->  f :
( M ... M
) --> ( M ... M ) )
5049adantr 276 . . . . . . . . . . . . 13  |-  ( ( f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C )  ->  f : ( M ... M ) --> ( M ... M
) )
51 elfz3 10090 . . . . . . . . . . . . 13  |-  ( M  e.  ZZ  ->  M  e.  ( M ... M
) )
52 fvco3 5620 . . . . . . . . . . . . 13  |-  ( ( f : ( M ... M ) --> ( M ... M )  /\  M  e.  ( M ... M ) )  ->  ( (
g  o.  f ) `
 M )  =  ( g `  (
f `  M )
) )
5350, 51, 52syl2anr 290 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  ( f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  -> 
( ( g  o.  f ) `  M
)  =  ( g `
 ( f `  M ) ) )
5453adantll 476 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  ( (
g  o.  f ) `
 M )  =  ( g `  (
f `  M )
) )
55 ffvelcdm 5683 . . . . . . . . . . . . . . . 16  |-  ( ( f : ( M ... M ) --> ( M ... M )  /\  M  e.  ( M ... M ) )  ->  ( f `  M )  e.  ( M ... M ) )
5649, 51, 55syl2anr 290 . . . . . . . . . . . . . . 15  |-  ( ( M  e.  ZZ  /\  f : ( M ... M ) -1-1-onto-> ( M ... M
) )  ->  (
f `  M )  e.  ( M ... M
) )
57 fzsn 10122 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
5857eleq2d 2263 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ZZ  ->  (
( f `  M
)  e.  ( M ... M )  <->  ( f `  M )  e.  { M } ) )
59 elsni 3636 . . . . . . . . . . . . . . . . 17  |-  ( ( f `  M )  e.  { M }  ->  ( f `  M
)  =  M )
6058, 59biimtrdi 163 . . . . . . . . . . . . . . . 16  |-  ( M  e.  ZZ  ->  (
( f `  M
)  e.  ( M ... M )  -> 
( f `  M
)  =  M ) )
6160imp 124 . . . . . . . . . . . . . . 15  |-  ( ( M  e.  ZZ  /\  ( f `  M
)  e.  ( M ... M ) )  ->  ( f `  M )  =  M )
6256, 61syldan 282 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  f : ( M ... M ) -1-1-onto-> ( M ... M
) )  ->  (
f `  M )  =  M )
6362adantrr 479 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  ( f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  -> 
( f `  M
)  =  M )
6463fveq2d 5550 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  ( f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  -> 
( g `  (
f `  M )
)  =  ( g `
 M ) )
6564adantll 476 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  ( g `  ( f `  M
) )  =  ( g `  M ) )
6654, 65eqtrd 2226 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  ( (
g  o.  f ) `
 M )  =  ( g `  M
) )
67 simplr 528 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  M  e.  ZZ )
68 vex 2763 . . . . . . . . . . . . 13  |-  g  e. 
_V
69 vex 2763 . . . . . . . . . . . . 13  |-  f  e. 
_V
7068, 69coex 5203 . . . . . . . . . . . 12  |-  ( g  o.  f )  e. 
_V
7170a1i 9 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  ( g  o.  f )  e.  _V )
72 seqf1og.p . . . . . . . . . . . 12  |-  ( ph  ->  .+  e.  V )
7372ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  .+  e.  V
)
74 seq1g 10524 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  ( g  o.  f
)  e.  _V  /\  .+  e.  V )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  M )  =  ( ( g  o.  f
) `  M )
)
7567, 71, 73, 74syl3anc 1249 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  M
)  =  ( ( g  o.  f ) `
 M ) )
7668a1i 9 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  g  e.  _V )
77 seq1g 10524 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  g  e.  _V  /\  .+  e.  V )  ->  (  seq M (  .+  , 
g ) `  M
)  =  ( g `
 M ) )
7867, 76, 73, 77syl3anc 1249 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  (  seq M (  .+  , 
g ) `  M
)  =  ( g `
 M ) )
7966, 75, 783eqtr4d 2236 . . . . . . . . 9  |-  ( ( ( ph  /\  M  e.  ZZ )  /\  (
f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C ) )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  M
)  =  (  seq M (  .+  , 
g ) `  M
) )
8079ex 115 . . . . . . . 8  |-  ( (
ph  /\  M  e.  ZZ )  ->  ( ( f : ( M ... M ) -1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  M )  =  (  seq M
(  .+  ,  g
) `  M )
) )
8180alrimivv 1886 . . . . . . 7  |-  ( (
ph  /\  M  e.  ZZ )  ->  A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M
)  /\  g :
( M ... M
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  M )  =  (  seq M (  .+  ,  g ) `  M ) ) )
8281expcom 116 . . . . . 6  |-  ( M  e.  ZZ  ->  ( ph  ->  A. g A. f
( ( f : ( M ... M
)
-1-1-onto-> ( M ... M )  /\  g : ( M ... M ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  M
)  =  (  seq M (  .+  , 
g ) `  M
) ) ) )
83 f1oeq1 5480 . . . . . . . . . . . 12  |-  ( f  =  t  ->  (
f : ( M ... k ) -1-1-onto-> ( M ... k )  <->  t :
( M ... k
)
-1-1-onto-> ( M ... k ) ) )
84 feq1 5378 . . . . . . . . . . . 12  |-  ( g  =  s  ->  (
g : ( M ... k ) --> C  <-> 
s : ( M ... k ) --> C ) )
8583, 84bi2anan9r 607 . . . . . . . . . . 11  |-  ( ( g  =  s  /\  f  =  t )  ->  ( ( f : ( M ... k
)
-1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  <->  ( t : ( M ... k ) -1-1-onto-> ( M ... k
)  /\  s :
( M ... k
) --> C ) ) )
86 coeq1 4813 . . . . . . . . . . . . . . 15  |-  ( g  =  s  ->  (
g  o.  f )  =  ( s  o.  f ) )
87 coeq2 4814 . . . . . . . . . . . . . . 15  |-  ( f  =  t  ->  (
s  o.  f )  =  ( s  o.  t ) )
8886, 87sylan9eq 2246 . . . . . . . . . . . . . 14  |-  ( ( g  =  s  /\  f  =  t )  ->  ( g  o.  f
)  =  ( s  o.  t ) )
8988seqeq3d 10516 . . . . . . . . . . . . 13  |-  ( ( g  =  s  /\  f  =  t )  ->  seq M (  .+  ,  ( g  o.  f ) )  =  seq M (  .+  ,  ( s  o.  t ) ) )
9089fveq1d 5548 . . . . . . . . . . . 12  |-  ( ( g  =  s  /\  f  =  t )  ->  (  seq M ( 
.+  ,  ( g  o.  f ) ) `
 k )  =  (  seq M ( 
.+  ,  ( s  o.  t ) ) `
 k ) )
91 simpl 109 . . . . . . . . . . . . . 14  |-  ( ( g  =  s  /\  f  =  t )  ->  g  =  s )
9291seqeq3d 10516 . . . . . . . . . . . . 13  |-  ( ( g  =  s  /\  f  =  t )  ->  seq M (  .+  ,  g )  =  seq M (  .+  ,  s ) )
9392fveq1d 5548 . . . . . . . . . . . 12  |-  ( ( g  =  s  /\  f  =  t )  ->  (  seq M ( 
.+  ,  g ) `
 k )  =  (  seq M ( 
.+  ,  s ) `
 k ) )
9490, 93eqeq12d 2208 . . . . . . . . . . 11  |-  ( ( g  =  s  /\  f  =  t )  ->  ( (  seq M
(  .+  ,  (
g  o.  f ) ) `  k )  =  (  seq M
(  .+  ,  g
) `  k )  <->  (  seq M (  .+  ,  ( s  o.  t ) ) `  k )  =  (  seq M (  .+  ,  s ) `  k ) ) )
9585, 94imbi12d 234 . . . . . . . . . 10  |-  ( ( g  =  s  /\  f  =  t )  ->  ( ( ( f : ( M ... k ) -1-1-onto-> ( M ... k
)  /\  g :
( M ... k
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  k )  =  (  seq M (  .+  ,  g ) `  k ) )  <->  ( (
t : ( M ... k ) -1-1-onto-> ( M ... k )  /\  s : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
s  o.  t ) ) `  k )  =  (  seq M
(  .+  ,  s
) `  k )
) ) )
9695cbval2vw 1944 . . . . . . . . 9  |-  ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  k )  =  (  seq M
(  .+  ,  g
) `  k )
)  <->  A. s A. t
( ( t : ( M ... k
)
-1-1-onto-> ( M ... k )  /\  s : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( s  o.  t
) ) `  k
)  =  (  seq M (  .+  , 
s ) `  k
) ) )
97 simplll 533 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  ->  ph )
98 seqf1o.1 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
9997, 98sylan 283 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  /\  ( x  e.  S  /\  y  e.  S
) )  ->  (
x  .+  y )  e.  S )
100 seqf1o.2 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  C  /\  y  e.  C ) )  -> 
( x  .+  y
)  =  ( y 
.+  x ) )
10197, 100sylan 283 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  /\  ( x  e.  C  /\  y  e.  C
) )  ->  (
x  .+  y )  =  ( y  .+  x ) )
102 seqf1o.3 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  -> 
( ( x  .+  y )  .+  z
)  =  ( x 
.+  ( y  .+  z ) ) )
10397, 102sylan 283 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S
) )  ->  (
( x  .+  y
)  .+  z )  =  ( x  .+  ( y  .+  z
) ) )
104 simpllr 534 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  -> 
k  e.  ( ZZ>= `  M ) )
105 seqf1o.5 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  C_  S )
10697, 105syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  ->  C  C_  S )
10797, 72syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  ->  .+  e.  V )
108 simprl 529 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  -> 
f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) ) )
109 simprr 531 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  -> 
g : ( M ... ( k  +  1 ) ) --> C )
110 eqid 2193 . . . . . . . . . . . . . 14  |-  ( w  e.  ( M ... k )  |->  ( f `
 if ( w  <  ( `' f `
 ( k  +  1 ) ) ,  w ,  ( w  +  1 ) ) ) )  =  ( w  e.  ( M ... k )  |->  ( f `  if ( w  <  ( `' f `  ( k  +  1 ) ) ,  w ,  ( w  +  1 ) ) ) )
111 eqid 2193 . . . . . . . . . . . . . 14  |-  ( `' f `  ( k  +  1 ) )  =  ( `' f `
 ( k  +  1 ) )
112 simplr 528 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  ->  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )
113112, 96sylib 122 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  ->  A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k )  /\  s : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( s  o.  t
) ) `  k
)  =  (  seq M (  .+  , 
s ) `  k
) ) )
11499, 101, 103, 104, 106, 107, 108, 109, 110, 111, 113seqf1oglem2 10581 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  /\  A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  /\  ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C ) )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) )
115114exp31 364 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  k )  =  (  seq M
(  .+  ,  g
) `  k )
)  ->  ( (
f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M
(  .+  ,  g
) `  ( k  +  1 ) ) ) ) )
11696, 115biimtrrid 153 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k )  /\  s : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
s  o.  t ) ) `  k )  =  (  seq M
(  .+  ,  s
) `  k )
)  ->  ( (
f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M
(  .+  ,  g
) `  ( k  +  1 ) ) ) ) )
117116alrimdv 1887 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k )  /\  s : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
s  o.  t ) ) `  k )  =  (  seq M
(  .+  ,  s
) `  k )
)  ->  A. f
( ( f : ( M ... (
k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) ) ) )
118117alrimdv 1887 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k )  /\  s : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
s  o.  t ) ) `  k )  =  (  seq M
(  .+  ,  s
) `  k )
)  ->  A. g A. f ( ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) ) ) )
11996, 118biimtrid 152 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M
(  .+  ,  (
g  o.  f ) ) `  k )  =  (  seq M
(  .+  ,  g
) `  k )
)  ->  A. g A. f ( ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) ) ) )
120119expcom 116 . . . . . . 7  |-  ( k  e.  ( ZZ>= `  M
)  ->  ( ph  ->  ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k
)  /\  g :
( M ... k
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  k )  =  (  seq M (  .+  ,  g ) `  k ) )  ->  A. g A. f ( ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... ( k  +  1 ) )  /\  g : ( M ... ( k  +  1 ) ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  (
k  +  1 ) )  =  (  seq M (  .+  , 
g ) `  (
k  +  1 ) ) ) ) ) )
121120a2d 26 . . . . . 6  |-  ( k  e.  ( ZZ>= `  M
)  ->  ( ( ph  ->  A. g A. f
( ( f : ( M ... k
)
-1-1-onto-> ( M ... k )  /\  g : ( M ... k ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  k
)  =  (  seq M (  .+  , 
g ) `  k
) ) )  -> 
( ph  ->  A. g A. f ( ( f : ( M ... ( k  +  1 ) ) -1-1-onto-> ( M ... (
k  +  1 ) )  /\  g : ( M ... (
k  +  1 ) ) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  ( k  +  1 ) )  =  (  seq M (  .+  ,  g ) `  ( k  +  1 ) ) ) ) ) )
12215, 26, 37, 48, 82, 121uzind4 9643 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ph  ->  A. g A. f
( ( f : ( M ... N
)
-1-1-onto-> ( M ... N )  /\  g : ( M ... N ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
g ) `  N
) ) ) )
1234, 122mpcom 36 . . . 4  |-  ( ph  ->  A. g A. f
( ( f : ( M ... N
)
-1-1-onto-> ( M ... N )  /\  g : ( M ... N ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
g ) `  N
) ) )
1242ralrimiva 2567 . . . . . . 7  |-  ( ph  ->  A. x  e.  ( M ... N ) ( G `  x
)  e.  C )
125 eqid 2193 . . . . . . . 8  |-  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  =  ( x  e.  ( M ... N
)  |->  ( G `  x ) )
126125fnmpt 5372 . . . . . . 7  |-  ( A. x  e.  ( M ... N ) ( G `
 x )  e.  C  ->  ( x  e.  ( M ... N
)  |->  ( G `  x ) )  Fn  ( M ... N
) )
127124, 126syl 14 . . . . . 6  |-  ( ph  ->  ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  Fn  ( M ... N ) )
128 eluzel2 9587 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
1294, 128syl 14 . . . . . . 7  |-  ( ph  ->  M  e.  ZZ )
130 eluzelz 9591 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
1314, 130syl 14 . . . . . . 7  |-  ( ph  ->  N  e.  ZZ )
132129, 131fzfigd 10492 . . . . . 6  |-  ( ph  ->  ( M ... N
)  e.  Fin )
133 fnfi 6985 . . . . . 6  |-  ( ( ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  Fn  ( M ... N )  /\  ( M ... N )  e.  Fin )  -> 
( x  e.  ( M ... N ) 
|->  ( G `  x
) )  e.  Fin )
134127, 132, 133syl2anc 411 . . . . 5  |-  ( ph  ->  ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  e.  Fin )
135 f1of 5492 . . . . . . 7  |-  ( F : ( M ... N ) -1-1-onto-> ( M ... N
)  ->  F :
( M ... N
) --> ( M ... N ) )
1361, 135syl 14 . . . . . 6  |-  ( ph  ->  F : ( M ... N ) --> ( M ... N ) )
137136, 132fexd 5780 . . . . 5  |-  ( ph  ->  F  e.  _V )
138 f1oeq1 5480 . . . . . . . 8  |-  ( f  =  F  ->  (
f : ( M ... N ) -1-1-onto-> ( M ... N )  <->  F :
( M ... N
)
-1-1-onto-> ( M ... N ) ) )
139 feq1 5378 . . . . . . . 8  |-  ( g  =  ( x  e.  ( M ... N
)  |->  ( G `  x ) )  -> 
( g : ( M ... N ) --> C  <->  ( x  e.  ( M ... N
)  |->  ( G `  x ) ) : ( M ... N
) --> C ) )
140138, 139bi2anan9r 607 . . . . . . 7  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  ( (
f : ( M ... N ) -1-1-onto-> ( M ... N )  /\  g : ( M ... N ) --> C )  <-> 
( F : ( M ... N ) -1-1-onto-> ( M ... N )  /\  ( x  e.  ( M ... N
)  |->  ( G `  x ) ) : ( M ... N
) --> C ) ) )
141 coeq1 4813 . . . . . . . . . . 11  |-  ( g  =  ( x  e.  ( M ... N
)  |->  ( G `  x ) )  -> 
( g  o.  f
)  =  ( ( x  e.  ( M ... N )  |->  ( G `  x ) )  o.  f ) )
142 coeq2 4814 . . . . . . . . . . 11  |-  ( f  =  F  ->  (
( x  e.  ( M ... N ) 
|->  ( G `  x
) )  o.  f
)  =  ( ( x  e.  ( M ... N )  |->  ( G `  x ) )  o.  F ) )
143141, 142sylan9eq 2246 . . . . . . . . . 10  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  ( g  o.  f )  =  ( ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  o.  F
) )
144143seqeq3d 10516 . . . . . . . . 9  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  seq M ( 
.+  ,  ( g  o.  f ) )  =  seq M ( 
.+  ,  ( ( x  e.  ( M ... N )  |->  ( G `  x ) )  o.  F ) ) )
145144fveq1d 5548 . . . . . . . 8  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
( ( x  e.  ( M ... N
)  |->  ( G `  x ) )  o.  F ) ) `  N ) )
146 simpl 109 . . . . . . . . . 10  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  g  =  ( x  e.  ( M ... N )  |->  ( G `  x ) ) )
147146seqeq3d 10516 . . . . . . . . 9  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  seq M ( 
.+  ,  g )  =  seq M ( 
.+  ,  ( x  e.  ( M ... N )  |->  ( G `
 x ) ) ) )
148147fveq1d 5548 . . . . . . . 8  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  (  seq M (  .+  , 
g ) `  N
)  =  (  seq M (  .+  , 
( x  e.  ( M ... N ) 
|->  ( G `  x
) ) ) `  N ) )
149145, 148eqeq12d 2208 . . . . . . 7  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  ( (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
g ) `  N
)  <->  (  seq M
(  .+  ,  (
( x  e.  ( M ... N ) 
|->  ( G `  x
) )  o.  F
) ) `  N
)  =  (  seq M (  .+  , 
( x  e.  ( M ... N ) 
|->  ( G `  x
) ) ) `  N ) ) )
150140, 149imbi12d 234 . . . . . 6  |-  ( ( g  =  ( x  e.  ( M ... N )  |->  ( G `
 x ) )  /\  f  =  F )  ->  ( (
( f : ( M ... N ) -1-1-onto-> ( M ... N )  /\  g : ( M ... N ) --> C )  ->  (  seq M (  .+  , 
( g  o.  f
) ) `  N
)  =  (  seq M (  .+  , 
g ) `  N
) )  <->  ( ( F : ( M ... N ) -1-1-onto-> ( M ... N
)  /\  ( x  e.  ( M ... N
)  |->  ( G `  x ) ) : ( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( ( x  e.  ( M ... N )  |->  ( G `
 x ) )  o.  F ) ) `
 N )  =  (  seq M ( 
.+  ,  ( x  e.  ( M ... N )  |->  ( G `
 x ) ) ) `  N ) ) ) )
151150spc2gv 2851 . . . . 5  |-  ( ( ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  e.  Fin  /\  F  e.  _V )  ->  ( A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N
)  /\  g :
( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  N )  =  (  seq M (  .+  ,  g ) `  N ) )  -> 
( ( F :
( M ... N
)
-1-1-onto-> ( M ... N )  /\  ( x  e.  ( M ... N
)  |->  ( G `  x ) ) : ( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( ( x  e.  ( M ... N )  |->  ( G `
 x ) )  o.  F ) ) `
 N )  =  (  seq M ( 
.+  ,  ( x  e.  ( M ... N )  |->  ( G `
 x ) ) ) `  N ) ) ) )
152134, 137, 151syl2anc 411 . . . 4  |-  ( ph  ->  ( A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N
)  /\  g :
( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( g  o.  f ) ) `  N )  =  (  seq M (  .+  ,  g ) `  N ) )  -> 
( ( F :
( M ... N
)
-1-1-onto-> ( M ... N )  /\  ( x  e.  ( M ... N
)  |->  ( G `  x ) ) : ( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( ( x  e.  ( M ... N )  |->  ( G `
 x ) )  o.  F ) ) `
 N )  =  (  seq M ( 
.+  ,  ( x  e.  ( M ... N )  |->  ( G `
 x ) ) ) `  N ) ) ) )
153123, 152mpd 13 . . 3  |-  ( ph  ->  ( ( F :
( M ... N
)
-1-1-onto-> ( M ... N )  /\  ( x  e.  ( M ... N
)  |->  ( G `  x ) ) : ( M ... N
) --> C )  -> 
(  seq M (  .+  ,  ( ( x  e.  ( M ... N )  |->  ( G `
 x ) )  o.  F ) ) `
 N )  =  (  seq M ( 
.+  ,  ( x  e.  ( M ... N )  |->  ( G `
 x ) ) ) `  N ) ) )
1541, 3, 153mp2and 433 . 2  |-  ( ph  ->  (  seq M ( 
.+  ,  ( ( x  e.  ( M ... N )  |->  ( G `  x ) )  o.  F ) ) `  N )  =  (  seq M
(  .+  ,  (
x  e.  ( M ... N )  |->  ( G `  x ) ) ) `  N
) )
155 fveq2 5546 . . . . 5  |-  ( x  =  ( F `  k )  ->  ( G `  x )  =  ( G `  ( F `  k ) ) )
156136ffvelcdmda 5685 . . . . 5  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( F `  k )  e.  ( M ... N ) )
157155eleq1d 2262 . . . . . 6  |-  ( x  =  ( F `  k )  ->  (
( G `  x
)  e.  C  <->  ( G `  ( F `  k
) )  e.  C
) )
158124adantr 276 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  A. x  e.  ( M ... N
) ( G `  x )  e.  C
)
159157, 158, 156rspcdva 2869 . . . . 5  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( G `  ( F `  k
) )  e.  C
)
160125, 155, 156, 159fvmptd3 5643 . . . 4  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( (
x  e.  ( M ... N )  |->  ( G `  x ) ) `  ( F `
 k ) )  =  ( G `  ( F `  k ) ) )
161 fvco3 5620 . . . . 5  |-  ( ( F : ( M ... N ) --> ( M ... N )  /\  k  e.  ( M ... N ) )  ->  ( (
( x  e.  ( M ... N ) 
|->  ( G `  x
) )  o.  F
) `  k )  =  ( ( x  e.  ( M ... N )  |->  ( G `
 x ) ) `
 ( F `  k ) ) )
162136, 161sylan 283 . . . 4  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( (
( x  e.  ( M ... N ) 
|->  ( G `  x
) )  o.  F
) `  k )  =  ( ( x  e.  ( M ... N )  |->  ( G `
 x ) ) `
 ( F `  k ) ) )
163 seqf1o.8 . . . 4  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( H `  k )  =  ( G `  ( F `
 k ) ) )
164160, 162, 1633eqtr4d 2236 . . 3  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( (
( x  e.  ( M ... N ) 
|->  ( G `  x
) )  o.  F
) `  k )  =  ( H `  k ) )
165134elexd 2773 . . . 4  |-  ( ph  ->  ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  e.  _V )
166 coexg 5202 . . . 4  |-  ( ( ( x  e.  ( M ... N ) 
|->  ( G `  x
) )  e.  _V  /\  F  e.  _V )  ->  ( ( x  e.  ( M ... N
)  |->  ( G `  x ) )  o.  F )  e.  _V )
167165, 137, 166syl2anc 411 . . 3  |-  ( ph  ->  ( ( x  e.  ( M ... N
)  |->  ( G `  x ) )  o.  F )  e.  _V )
168 seqf1og.h . . 3  |-  ( ph  ->  H  e.  X )
1694, 164, 72, 167, 168seqfveqg 10539 . 2  |-  ( ph  ->  (  seq M ( 
.+  ,  ( ( x  e.  ( M ... N )  |->  ( G `  x ) )  o.  F ) ) `  N )  =  (  seq M
(  .+  ,  H
) `  N )
)
170 fveq2 5546 . . . 4  |-  ( x  =  k  ->  ( G `  x )  =  ( G `  k ) )
171 simpr 110 . . . 4  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  k  e.  ( M ... N ) )
172170eleq1d 2262 . . . . 5  |-  ( x  =  k  ->  (
( G `  x
)  e.  C  <->  ( G `  k )  e.  C
) )
173172, 158, 171rspcdva 2869 . . . 4  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( G `  k )  e.  C
)
174125, 170, 171, 173fvmptd3 5643 . . 3  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( (
x  e.  ( M ... N )  |->  ( G `  x ) ) `  k )  =  ( G `  k ) )
175 seqf1og.g . . 3  |-  ( ph  ->  G  e.  W )
1764, 174, 72, 134, 175seqfveqg 10539 . 2  |-  ( ph  ->  (  seq M ( 
.+  ,  ( x  e.  ( M ... N )  |->  ( G `
 x ) ) ) `  N )  =  (  seq M
(  .+  ,  G
) `  N )
)
177154, 169, 1763eqtr3d 2234 1  |-  ( ph  ->  (  seq M ( 
.+  ,  H ) `
 N )  =  (  seq M ( 
.+  ,  G ) `
 N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    /\ w3a 980   A.wal 1362    = wceq 1364    e. wcel 2164   A.wral 2472   _Vcvv 2760    C_ wss 3153   ifcif 3557   {csn 3618   class class class wbr 4029    |-> cmpt 4090   `'ccnv 4654    o. ccom 4659    Fn wfn 5241   -->wf 5242   -1-1-onto->wf1o 5245   ` cfv 5246  (class class class)co 5910   Fincfn 6785   1c1 7863    + caddc 7865    < clt 8044   ZZcz 9307   ZZ>=cuz 9582   ...cfz 10064    seqcseq 10508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-iinf 4616  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-mulrcl 7961  ax-addcom 7962  ax-mulcom 7963  ax-addass 7964  ax-mulass 7965  ax-distr 7966  ax-i2m1 7967  ax-0lt1 7968  ax-1rid 7969  ax-0id 7970  ax-rnegex 7971  ax-precex 7972  ax-cnre 7973  ax-pre-ltirr 7974  ax-pre-ltwlin 7975  ax-pre-lttrn 7976  ax-pre-apti 7977  ax-pre-ltadd 7978  ax-pre-mulgt0 7979
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4322  df-iord 4395  df-on 4397  df-ilim 4398  df-suc 4400  df-iom 4619  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-f 5250  df-f1 5251  df-fo 5252  df-f1o 5253  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-1st 6184  df-2nd 6185  df-recs 6349  df-frec 6435  df-1o 6460  df-er 6578  df-en 6786  df-fin 6788  df-pnf 8046  df-mnf 8047  df-xr 8048  df-ltxr 8049  df-le 8050  df-sub 8182  df-neg 8183  df-reap 8584  df-ap 8591  df-inn 8973  df-n0 9231  df-z 9308  df-uz 9583  df-fz 10065  df-fzo 10199  df-seqfrec 10509
This theorem is referenced by:  gsumfzreidx  13396
  Copyright terms: Public domain W3C validator