Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clwlkfclwwlk Structured version   Unicode version

Theorem clwlkfclwwlk 30658
Description: There is a function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 25-Jun-2018.)
Hypotheses
Ref Expression
clwlkfclwwlk.1  |-  A  =  ( 1st `  c
)
clwlkfclwwlk.2  |-  B  =  ( 2nd `  c
)
clwlkfclwwlk.c  |-  C  =  { c  e.  ( V ClWalks  E )  |  (
# `  A )  =  N }
clwlkfclwwlk.f  |-  F  =  ( c  e.  C  |->  ( B substr  <. 0 ,  ( # `  A
) >. ) )
Assertion
Ref Expression
clwlkfclwwlk  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  F : C
--> ( ( V ClWWalksN  E ) `
 N ) )
Distinct variable groups:    E, c    N, c    V, c    C, c
Allowed substitution hints:    A( c)    B( c)    F( c)

Proof of Theorem clwlkfclwwlk
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 clwlkfclwwlk.c . . . . . 6  |-  C  =  { c  e.  ( V ClWalks  E )  |  (
# `  A )  =  N }
21rabeq2i 3068 . . . . 5  |-  ( c  e.  C  <->  ( c  e.  ( V ClWalks  E )  /\  ( # `  A
)  =  N ) )
3 clwlkfclwwlk.1 . . . . . . . 8  |-  A  =  ( 1st `  c
)
4 clwlkfclwwlk.2 . . . . . . . 8  |-  B  =  ( 2nd `  c
)
53, 4clwlkcompim 30568 . . . . . . 7  |-  ( c  e.  ( V ClWalks  E
)  ->  ( ( A  e. Word  dom  E  /\  B : ( 0 ... ( # `  A
) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A ) ) ( E `  ( A `
 i ) )  =  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  /\  ( B `  0 )  =  ( B `  ( # `  A ) ) ) ) )
6 lencl 12360 . . . . . . . . 9  |-  ( A  e. Word  dom  E  ->  (
# `  A )  e.  NN0 )
7 clwlkfclwwlk.f . . . . . . . . . . . . . . . . . 18  |-  F  =  ( c  e.  C  |->  ( B substr  <. 0 ,  ( # `  A
) >. ) )
83, 4, 1, 7clwlkfclwwlk2wrd 30654 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  C  ->  B  e. Word  V )
98ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  B  e. Word  V )
10 swrdcl 12426 . . . . . . . . . . . . . . . 16  |-  ( B  e. Word  V  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e. Word  V )
119, 10syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e. Word  V )
12 simp-5r 768 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  A  e. Word  dom  E )
13 simp1 988 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  V USGrph  E )
1412, 13anim12ci 567 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( V USGrph  E  /\  A  e. Word  dom  E ) )
15 simp-5r 768 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  B : ( 0 ... ( # `  A
) ) --> V )
16 prmuz2 13892 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  Prime  ->  N  e.  ( ZZ>= `  2 )
)
17 hashfzdm 12313 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  A
)  e.  NN0  /\  B : ( 0 ... ( # `  A
) ) --> V )  ->  ( # `  B
)  =  ( (
# `  A )  +  1 ) )
1817adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  ->  ( # `  B
)  =  ( (
# `  A )  +  1 ) )
19 eluz2 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  A )  e.  ( ZZ>= `  2 )  <->  ( 2  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  2  <_  ( # `  A
) ) )
20 2re 10495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  2  e.  RR
2120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  2  e.  RR )
22 zre 10754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  RR )
23 peano2re 9646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
# `  A )  e.  RR  ->  ( ( # `
 A )  +  1 )  e.  RR )
2422, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  +  1 )  e.  RR )
2521, 22, 243jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( 2  e.  RR  /\  ( # `
 A )  e.  RR  /\  ( (
# `  A )  +  1 )  e.  RR ) )
2625adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  (
2  e.  RR  /\  ( # `  A )  e.  RR  /\  (
( # `  A )  +  1 )  e.  RR ) )
27 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( # `  A
) )
2822lep1d 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  <_  ( ( # `
 A )  +  1 ) )
2928adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  ( # `
 A )  <_ 
( ( # `  A
)  +  1 ) )
30 letr 9572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 2  e.  RR  /\  ( # `  A )  e.  RR  /\  (
( # `  A )  +  1 )  e.  RR )  ->  (
( 2  <_  ( # `
 A )  /\  ( # `  A )  <_  ( ( # `  A )  +  1 ) )  ->  2  <_  ( ( # `  A
)  +  1 ) ) )
3130imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 2  e.  RR  /\  ( # `  A
)  e.  RR  /\  ( ( # `  A
)  +  1 )  e.  RR )  /\  ( 2  <_  ( # `
 A )  /\  ( # `  A )  <_  ( ( # `  A )  +  1 ) ) )  -> 
2  <_  ( ( # `
 A )  +  1 ) )
3226, 27, 29, 31syl12anc 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( ( # `  A
)  +  1 ) )
33323adant1 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( ( # `  A
)  +  1 ) )
3419, 33sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  A )  e.  ( ZZ>= `  2 )  ->  2  <_  ( ( # `
 A )  +  1 ) )
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( ( # `  A
)  e.  ( ZZ>= ` 
2 )  ->  2  <_  ( ( # `  A
)  +  1 ) ) )
36 eleq1 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  =  ( # `  A
)  ->  ( N  e.  ( ZZ>= `  2 )  <->  (
# `  A )  e.  ( ZZ>= `  2 )
) )
3736eqcoms 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  A )  =  N  ->  ( N  e.  ( ZZ>= `  2
)  <->  ( # `  A
)  e.  ( ZZ>= ` 
2 ) ) )
3837adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( N  e.  (
ZZ>= `  2 )  <->  ( # `  A
)  e.  ( ZZ>= ` 
2 ) ) )
39 breq2 4397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  B )  =  ( ( # `  A )  +  1 )  ->  ( 2  <_  ( # `  B
)  <->  2  <_  (
( # `  A )  +  1 ) ) )
4039adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( 2  <_  ( # `
 B )  <->  2  <_  ( ( # `  A
)  +  1 ) ) )
4135, 38, 403imtr4d 268 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( N  e.  (
ZZ>= `  2 )  -> 
2  <_  ( # `  B
) ) )
4241ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  B )  =  ( ( # `  A )  +  1 )  ->  ( ( # `
 A )  =  N  ->  ( N  e.  ( ZZ>= `  2 )  ->  2  <_  ( # `  B
) ) ) )
4318, 42syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  ->  ( ( # `
 A )  =  N  ->  ( N  e.  ( ZZ>= `  2 )  ->  2  <_  ( # `  B
) ) ) )
4443adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( # `  A )  e.  NN0  /\  A  e. Word  dom  E
)  /\  B :
( 0 ... ( # `
 A ) ) --> V )  /\  ( A. i  e.  (
0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  ->  (
( # `  A )  =  N  ->  ( N  e.  ( ZZ>= ` 
2 )  ->  2  <_  ( # `  B
) ) ) )
4544imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
# `  A )  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A
) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A ) ) ( E `  ( A `
 i ) )  =  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  /\  ( B `  0 )  =  ( B `  ( # `  A ) ) ) )  /\  ( # `  A )  =  N )  -> 
( N  e.  (
ZZ>= `  2 )  -> 
2  <_  ( # `  B
) ) )
4645adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  ( N  e.  ( ZZ>= ` 
2 )  ->  2  <_  ( # `  B
) ) )
4716, 46syl5com 30 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  Prime  ->  ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  2  <_  ( # `  B
) ) )
48473ad2ant3 1011 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( (
( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  2  <_  ( # `  B
) ) )
4948impcom 430 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  2  <_  ( # `  B
) )
50 simp-4r 766 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( A. i  e.  (
0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )
51 clwlkisclwwlklem1 30590 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( V USGrph  E  /\  A  e. Word  dom  E )  /\  ( B :
( 0 ... ( # `
 A ) ) --> V  /\  2  <_ 
( # `  B ) )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  ->  (
( lastS  `  B )  =  ( B `  0
)  /\  A. i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  e.  ran  E ) )
5214, 15, 49, 50, 51syl121anc 1224 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( lastS  `  B )  =  ( B `  0
)  /\  A. i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  e.  ran  E ) )
533, 4, 1, 7clwlkfclwwlk1hash 30656 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  e.  C  ->  ( # `
 A )  e.  ( 0 ... ( # `
 B ) ) )
54 simp2 989 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  B  e. Word  V )
55 simp1 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( # `  A
)  e.  ( 0 ... ( # `  B
) ) )
56 elfzelz 11563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( # `  A
)  e.  ZZ )
57 peano2zm 10792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  - 
1 )  e.  ZZ )
58 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  ZZ )
5922lem1d 10370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  - 
1 )  <_  ( # `
 A ) )
60 eluz2 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ( ZZ>= `  ( ( # `
 A )  - 
1 ) )  <->  ( (
( # `  A )  -  1 )  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  ( ( # `  A
)  -  1 )  <_  ( # `  A
) ) )
6157, 58, 59, 60syl3anbrc 1172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  ( ZZ>= `  ( ( # `  A
)  -  1 ) ) )
62 fzoss2 11687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( ZZ>= `  ( ( # `
 A )  - 
1 ) )  -> 
( 0..^ ( (
# `  A )  -  1 ) ) 
C_  ( 0..^ (
# `  A )
) )
6356, 61, 623syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( 0..^ ( ( # `  A
)  -  1 ) )  C_  ( 0..^ ( # `  A
) ) )
6463sselda 3457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  i  e.  ( 0..^ ( # `  A
) ) )
65643adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  i  e.  ( 0..^ ( # `  A
) ) )
66 swrd0fv 12446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  i )  =  ( B `  i ) )
6754, 55, 65, 66syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  i )  =  ( B `  i ) )
6867eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( B `  i )  =  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) )
69 elfzom1elp1fzo 30359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  A
)  e.  ZZ  /\  i  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )  ->  (
i  +  1 )  e.  ( 0..^ (
# `  A )
) )
7056, 69sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( # `  A ) ) )
71703adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( # `  A ) ) )
72 swrd0fv 12446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  (
i  +  1 )  e.  ( 0..^ (
# `  A )
) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) )  =  ( B `
 ( i  +  1 ) ) )
7372eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  (
i  +  1 )  e.  ( 0..^ (
# `  A )
) )  ->  ( B `  ( i  +  1 ) )  =  ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  ( i  +  1 ) ) )
7454, 55, 71, 73syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( B `  ( i  +  1 ) )  =  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) ) )
7568, 74preq12d 4063 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  =  { ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  i ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) ) } )
76753exp 1187 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( B  e. Word  V  ->  ( i  e.  ( 0..^ ( (
# `  A )  -  1 ) )  ->  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  =  {
( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) } ) ) )
7753, 8, 76sylc 60 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  e.  C  ->  (
i  e.  ( 0..^ ( ( # `  A
)  -  1 ) )  ->  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  =  { ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  i ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) ) } ) )
7877imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( c  e.  C  /\  i  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )  ->  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  =  { ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  i ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) ) } )
7978eleq1d 2520 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c  e.  C  /\  i  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )  ->  ( { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E
) )
8079ralbidva 2839 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  e.  C  ->  ( A. i  e.  (
0..^ ( ( # `  A )  -  1 ) ) { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( ( # `  A )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E
) )
8180ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( A. i  e.  (
0..^ ( ( # `  A )  -  1 ) ) { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( ( # `  A )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E
) )
823, 4, 1, 7clwlkfclwwlk2sswd 30657 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  e.  C  ->  ( # `
 A )  =  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) )
8382oveq1d 6208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  e.  C  ->  (
( # `  A )  -  1 )  =  ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) )
8483ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( # `  A )  -  1 )  =  ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) )
8584oveq2d 6209 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
0..^ ( ( # `  A )  -  1 ) )  =  ( 0..^ ( ( # `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  - 
1 ) ) )
8685raleqdv 3022 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( A. i  e.  (
0..^ ( ( # `  A )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E
) )
8781, 86bitrd 253 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( A. i  e.  (
0..^ ( ( # `  A )  -  1 ) ) { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  - 
1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E
) )
88 eleq1 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  =  ( # `  A
)  ->  ( N  e.  Prime 
<->  ( # `  A
)  e.  Prime )
)
8988biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  =  ( # `  A
)  ->  ( N  e.  Prime  ->  ( # `  A
)  e.  Prime )
)
9089eqcoms 2463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  A )  =  N  ->  ( N  e.  Prime  ->  ( # `  A )  e.  Prime ) )
91 prmnn 13877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  A )  e.  Prime  ->  ( # `  A
)  e.  NN )
92 elfz2nn0 11590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  <-> 
( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) ) )
93 1z 10780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  1  e.  ZZ
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
1  e.  ZZ )
95 nn0z 10773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  B )  e.  NN0  ->  ( # `  B
)  e.  ZZ )
9695adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( # `  B )  e.  ZZ )
97 nn0z 10773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  A )  e.  NN0  ->  ( # `  A
)  e.  ZZ )
9897adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( # `  A )  e.  ZZ )
9994, 96, 983jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( 1  e.  ZZ  /\  ( # `  B
)  e.  ZZ  /\  ( # `  A )  e.  ZZ ) )
100993adant3 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( 1  e.  ZZ  /\  ( # `
 B )  e.  ZZ  /\  ( # `  A )  e.  ZZ ) )
101100adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( 1  e.  ZZ  /\  ( # `  B )  e.  ZZ  /\  ( # `  A
)  e.  ZZ ) )
102 simp3 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( # `  A
)  <_  ( # `  B
) )
103 nnge1 10452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
# `  A )  e.  NN  ->  1  <_  (
# `  A )
)
104102, 103anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) )
105101, 104jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( ( 1  e.  ZZ  /\  ( # `
 B )  e.  ZZ  /\  ( # `  A )  e.  ZZ )  /\  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) ) )
10692, 105sylanb 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  (
( 1  e.  ZZ  /\  ( # `  B
)  e.  ZZ  /\  ( # `  A )  e.  ZZ )  /\  ( 1  <_  ( # `
 A )  /\  ( # `  A )  <_  ( # `  B
) ) ) )
107 elfz2 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ( 1 ... ( # `
 B ) )  <-> 
( ( 1  e.  ZZ  /\  ( # `  B )  e.  ZZ  /\  ( # `  A
)  e.  ZZ )  /\  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) ) )
108106, 107sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  ( # `
 A )  e.  ( 1 ... ( # `
 B ) ) )
109 swrd0fvlsw 12450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  ( B `  (
( # `  A )  -  1 ) ) )
110109eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B `  (
( # `  A )  -  1 ) )  =  ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) )
111 swrd0fv0 12447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
)  =  ( B `
 0 ) )
112111eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B `  0
)  =  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) )
113110, 112preq12d 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  ->  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } )
114113expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( 1 ... ( # `
 B ) )  ->  ( B  e. Word  V  ->  { ( B `
 ( ( # `  A )  -  1 ) ) ,  ( B `  0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } ) )
115108, 114syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  ( B  e. Word  V  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
116115ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( ( # `  A )  e.  NN  ->  ( B  e. Word  V  ->  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } ) ) )
117116com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( B  e. Word  V  ->  ( ( # `  A )  e.  NN  ->  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } ) ) )
11853, 8, 117sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  C  ->  (
( # `  A )  e.  NN  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
11991, 118syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  A )  e.  Prime  ->  ( c  e.  C  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
12090, 119syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  A )  =  N  ->  ( N  e.  Prime  ->  ( c  e.  C  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) ) )
121120com23 78 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  A )  =  N  ->  ( c  e.  C  ->  ( N  e.  Prime  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) ) )
122121adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
# `  A )  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A
) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A ) ) ( E `  ( A `
 i ) )  =  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  /\  ( B `  0 )  =  ( B `  ( # `  A ) ) ) )  /\  ( # `  A )  =  N )  -> 
( c  e.  C  ->  ( N  e.  Prime  ->  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } ) ) )
123122imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  ( N  e.  Prime  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
124123com12 31 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  Prime  ->  ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
1251243ad2ant3 1011 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( (
( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
126125impcom 430 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } )
127126eleq1d 2520 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  e.  ran  E  <->  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) )
12887, 1273anbi23d 1293 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( ( lastS  `  B
)  =  ( B `
 0 )  /\  A. i  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( B `
 ( ( # `  A )  -  1 ) ) ,  ( B `  0 ) }  e.  ran  E
)  <->  ( ( lastS  `  B
)  =  ( B `
 0 )  /\  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) ) )
12952, 128mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( lastS  `  B )  =  ( B `  0
)  /\  A. i  e.  ( 0..^ ( (
# `  ( B substr  <.
0 ,  ( # `  A ) >. )
)  -  1 ) ) { ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  i ) ,  ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) )
130 3simpc 987 . . . . . . . . . . . . . . . 16  |-  ( ( ( lastS  `  B )  =  ( B ` 
0 )  /\  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E )  ->  ( A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) )
131129, 130syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( A. i  e.  (
0..^ ( ( # `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  - 
1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) )
132 3anass 969 . . . . . . . . . . . . . . 15  |-  ( ( ( B substr  <. 0 ,  ( # `  A
) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  - 
1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E )  <->  ( ( B substr  <. 0 ,  ( # `  A ) >. )  e. Word  V  /\  ( A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) ) )
13311, 131, 132sylanbrc 664 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  - 
1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) )
134 usgrav 23415 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
1351343ad2ant1 1009 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( V  e.  _V  /\  E  e. 
_V ) )
136135adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( V  e.  _V  /\  E  e.  _V ) )
137 isclwwlk 30572 . . . . . . . . . . . . . . 15  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( ( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( V ClWWalks  E )  <->  ( ( B substr  <. 0 ,  (
# `  A ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) ) )
138136, 137syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( V ClWWalks  E )  <->  ( ( B substr  <. 0 ,  (
# `  A ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) ) { ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) }  e.  ran  E ) ) )
139133, 138mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( V ClWWalks  E ) )
14082eqeq1d 2453 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  C  ->  (
( # `  A )  =  N  <->  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  =  N ) )
141140biimpcd 224 . . . . . . . . . . . . . . . 16  |-  ( (
# `  A )  =  N  ->  ( c  e.  C  ->  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N ) )
142141adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
# `  A )  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A
) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A ) ) ( E `  ( A `
 i ) )  =  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  /\  ( B `  0 )  =  ( B `  ( # `  A ) ) ) )  /\  ( # `  A )  =  N )  -> 
( c  e.  C  ->  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  =  N ) )
143142imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  ->  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N )
144143adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N )
145139, 144jca 532 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( V ClWWalks  E )  /\  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N ) )
146134simpld 459 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  V  e.  _V )
147146adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  V  e. 
_V )
148134simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  E  e.  _V )
149148adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  E  e. 
_V )
150 prmnn 13877 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  Prime  ->  N  e.  NN )
151150nnnn0d 10740 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  Prime  ->  N  e. 
NN0 )
152151adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  N  e. 
NN0 )
153147, 149, 1523jca 1168 . . . . . . . . . . . . . . 15  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  ( V  e.  _V  /\  E  e.  _V  /\  N  e. 
NN0 ) )
1541533adant2 1007 . . . . . . . . . . . . . 14  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( V  e.  _V  /\  E  e. 
_V  /\  N  e.  NN0 ) )
155154adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( V  e.  _V  /\  E  e.  _V  /\  N  e. 
NN0 ) )
156 isclwwlkn 30573 . . . . . . . . . . . . 13  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  N  e.  NN0 )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N )  <->  ( ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( V ClWWalks  E )  /\  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N ) ) )
157155, 156syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N )  <->  ( ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( V ClWWalks  E )  /\  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N ) ) )
158145, 157mpbird 232 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  /\  ( # `
 A )  =  N )  /\  c  e.  C )  /\  ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime ) )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) )
159158exp31 604 . . . . . . . . . 10  |-  ( ( ( ( ( (
# `  A )  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A
) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A ) ) ( E `  ( A `
 i ) )  =  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  /\  ( B `  0 )  =  ( B `  ( # `  A ) ) ) )  /\  ( # `  A )  =  N )  -> 
( c  e.  C  ->  ( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N ) ) ) )
160159exp41 610 . . . . . . . . 9  |-  ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  ->  ( B :
( 0 ... ( # `
 A ) ) --> V  ->  ( ( A. i  e.  (
0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) )  ->  ( ( # `
 A )  =  N  ->  ( c  e.  C  ->  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( B substr  <.
0 ,  ( # `  A ) >. )  e.  ( ( V ClWWalksN  E ) `
 N ) ) ) ) ) ) )
1616, 160mpancom 669 . . . . . . . 8  |-  ( A  e. Word  dom  E  ->  ( B : ( 0 ... ( # `  A
) ) --> V  -> 
( ( A. i  e.  ( 0..^ ( # `  A ) ) ( E `  ( A `
 i ) )  =  { ( B `
 i ) ,  ( B `  (
i  +  1 ) ) }  /\  ( B `  0 )  =  ( B `  ( # `  A ) ) )  ->  (
( # `  A )  =  N  ->  (
c  e.  C  -> 
( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N ) ) ) ) ) ) )
162161imp31 432 . . . . . . 7  |-  ( ( ( A  e. Word  dom  E  /\  B : ( 0 ... ( # `  A ) ) --> V )  /\  ( A. i  e.  ( 0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )  ->  (
( # `  A )  =  N  ->  (
c  e.  C  -> 
( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N ) ) ) ) )
1635, 162syl 16 . . . . . 6  |-  ( c  e.  ( V ClWalks  E
)  ->  ( ( # `
 A )  =  N  ->  ( c  e.  C  ->  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( B substr  <.
0 ,  ( # `  A ) >. )  e.  ( ( V ClWWalksN  E ) `
 N ) ) ) ) )
164163imp 429 . . . . 5  |-  ( ( c  e.  ( V ClWalks  E )  /\  ( # `
 A )  =  N )  ->  (
c  e.  C  -> 
( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N ) ) ) )
1652, 164sylbi 195 . . . 4  |-  ( c  e.  C  ->  (
c  e.  C  -> 
( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  ( # `  A
) >. )  e.  ( ( V ClWWalksN  E ) `  N ) ) ) )
166165pm2.43i 47 . . 3  |-  ( c  e.  C  ->  (
( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) ) )
167166impcom 430 . 2  |-  ( ( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  /\  c  e.  C )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) )
168167, 7fmptd 5969 1  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  F : C
--> ( ( V ClWWalksN  E ) `
 N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758   A.wral 2795   {crab 2799   _Vcvv 3071    C_ wss 3429   {cpr 3980   <.cop 3984   class class class wbr 4393    |-> cmpt 4451   dom cdm 4941   ran crn 4942   -->wf 5515   ` cfv 5519  (class class class)co 6193   1stc1st 6678   2ndc2nd 6679   Fincfn 7413   RRcr 9385   0cc0 9386   1c1 9387    + caddc 9389    <_ cle 9523    - cmin 9699   NNcn 10426   2c2 10475   NN0cn0 10683   ZZcz 10750   ZZ>=cuz 10965   ...cfz 11547  ..^cfzo 11658   #chash 12213  Word cword 12332   lastS clsw 12333   substr csubstr 12336   Primecprime 13874   USGrph cusg 23409   ClWalks cclwlk 30553   ClWWalks cclwwlk 30554   ClWWalksN cclwwlkn 30555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-cnex 9442  ax-resscn 9443  ax-1cn 9444  ax-icn 9445  ax-addcl 9446  ax-addrcl 9447  ax-mulcl 9448  ax-mulrcl 9449  ax-mulcom 9450  ax-addass 9451  ax-mulass 9452  ax-distr 9453  ax-i2m1 9454  ax-1ne0 9455  ax-1rid 9456  ax-rnegex 9457  ax-rrecex 9458  ax-cnre 9459  ax-pre-lttri 9460  ax-pre-lttrn 9461  ax-pre-ltadd 9462  ax-pre-mulgt0 9463
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-pss 3445  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-tp 3983  df-op 3985  df-uni 4193  df-int 4230  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-tr 4487  df-eprel 4733  df-id 4737  df-po 4742  df-so 4743  df-fr 4780  df-we 4782  df-ord 4823  df-on 4824  df-lim 4825  df-suc 4826  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-riota 6154  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-om 6580  df-1st 6680  df-2nd 6681  df-recs 6935  df-rdg 6969  df-1o 7023  df-2o 7024  df-oadd 7027  df-er 7204  df-map 7319  df-pm 7320  df-en 7414  df-dom 7415  df-sdom 7416  df-fin 7417  df-card 8213  df-cda 8441  df-pnf 9524  df-mnf 9525  df-xr 9526  df-ltxr 9527  df-le 9528  df-sub 9701  df-neg 9702  df-nn 10427  df-2 10484  df-n0 10684  df-z 10751  df-uz 10966  df-fz 11548  df-fzo 11659  df-hash 12214  df-word 12340  df-lsw 12341  df-substr 12344  df-dvds 13647  df-prm 13875  df-usgra 23411  df-wlk 23560  df-clwlk 30556  df-clwwlk 30557  df-clwwlkn 30558
This theorem is referenced by:  clwlkfoclwwlk  30659  clwlkf1clwwlk  30664
  Copyright terms: Public domain W3C validator