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

Theorem clwlkfclwwlk 25509
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 3014 . . . . 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 25429 . . . . . . 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 12630 . . . . . . . . 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 25505 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  C  ->  B  e. Word  V )
98ad2antlr 731 . . . . . . . . . . . . . . . 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 12716 . . . . . . . . . . . . . . . 16  |-  ( B  e. Word  V  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e. Word  V )
119, 10syl 17 . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . . . . . 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 1005 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  V USGrph  E )
1412, 13anim12ci 569 . . . . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . . . . 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 14580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  Prime  ->  N  e.  ( ZZ>= `  2 )
)
17 hashfzdm 12555 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  A
)  e.  NN0  /\  B : ( 0 ... ( # `  A
) ) --> V )  ->  ( # `  B
)  =  ( (
# `  A )  +  1 ) )
1817adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  ->  ( # `  B
)  =  ( (
# `  A )  +  1 ) )
19 eluz2 11111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  A )  e.  ( ZZ>= `  2 )  <->  ( 2  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  2  <_  ( # `  A
) ) )
20 2re 10625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  2  e.  RR
2120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  2  e.  RR )
22 zre 10887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  RR )
23 peano2re 9752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
# `  A )  e.  RR  ->  ( ( # `
 A )  +  1 )  e.  RR )
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  +  1 )  e.  RR )
2521, 22, 243jca 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( 2  e.  RR  /\  ( # `
 A )  e.  RR  /\  ( (
# `  A )  +  1 )  e.  RR ) )
2625adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  (
2  e.  RR  /\  ( # `  A )  e.  RR  /\  (
( # `  A )  +  1 )  e.  RR ) )
27 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( # `  A
) )
2822lep1d 10484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  <_  ( ( # `
 A )  +  1 ) )
2928adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  ( # `
 A )  <_ 
( ( # `  A
)  +  1 ) )
30 letr 9673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 2  e.  RR  /\  ( # `  A )  e.  RR  /\  (
( # `  A )  +  1 )  e.  RR )  ->  (
( 2  <_  ( # `
 A )  /\  ( # `  A )  <_  ( ( # `  A )  +  1 ) )  ->  2  <_  ( ( # `  A
)  +  1 ) ) )
3130imp 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 2  e.  RR  /\  ( # `  A
)  e.  RR  /\  ( ( # `  A
)  +  1 )  e.  RR )  /\  ( 2  <_  ( # `
 A )  /\  ( # `  A )  <_  ( ( # `  A )  +  1 ) ) )  -> 
2  <_  ( ( # `
 A )  +  1 ) )
3226, 27, 29, 31syl12anc 1262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( ( # `  A
)  +  1 ) )
33323adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( ( # `  A
)  +  1 ) )
3419, 33sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  =  ( # `  A
)  ->  ( N  e.  ( ZZ>= `  2 )  <->  (
# `  A )  e.  ( ZZ>= `  2 )
) )
3736eqcoms 2431 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  A )  =  N  ->  ( N  e.  ( ZZ>= `  2
)  <->  ( # `  A
)  e.  ( ZZ>= ` 
2 ) ) )
3837adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( N  e.  (
ZZ>= `  2 )  <->  ( # `  A
)  e.  ( ZZ>= ` 
2 ) ) )
39 breq2 4365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  B )  =  ( ( # `  A )  +  1 )  ->  ( 2  <_  ( # `  B
)  <->  2  <_  (
( # `  A )  +  1 ) ) )
4039adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( 2  <_  ( # `
 B )  <->  2  <_  ( ( # `  A
)  +  1 ) ) )
4135, 38, 403imtr4d 271 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  B
)  =  ( (
# `  A )  +  1 )  /\  ( # `  A )  =  N )  -> 
( N  e.  (
ZZ>= `  2 )  -> 
2  <_  ( # `  B
) ) )
4241ex 435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  B )  =  ( ( # `  A )  +  1 )  ->  ( ( # `
 A )  =  N  ->  ( N  e.  ( ZZ>= `  2 )  ->  2  <_  ( # `  B
) ) ) )
4318, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( # `  A
)  e.  NN0  /\  A  e. Word  dom  E )  /\  B : ( 0 ... ( # `  A ) ) --> V )  ->  ( ( # `
 A )  =  N  ->  ( N  e.  ( ZZ>= `  2 )  ->  2  <_  ( # `  B
) ) ) )
4443adantr 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  ->  ( N  e.  ( ZZ>= ` 
2 )  ->  2  <_  ( # `  B
) ) ) )
4544imp 430 . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . . . . . . 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 1028 . . . . . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . . . . . 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 775 . . . . . . . . . . . . . . . . . 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 25452 . . . . . . . . . . . . . . . . . 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 1269 . . . . . . . . . . . . . . . . 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 25507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  e.  C  ->  ( # `
 A )  e.  ( 0 ... ( # `
 B ) ) )
54 simp2 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  B  e. Word  V )
55 simp1 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( # `  A
)  e.  ( 0 ... ( # `  B
) ) )
56 elfzelz 11746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( # `  A
)  e.  ZZ )
57 peano2zm 10926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  - 
1 )  e.  ZZ )
58 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  ZZ )
5922lem1d 10486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  - 
1 )  <_  ( # `
 A ) )
60 eluz2 11111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ( ZZ>= `  ( ( # `
 A )  - 
1 ) )  <->  ( (
( # `  A )  -  1 )  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  ( ( # `  A
)  -  1 )  <_  ( # `  A
) ) )
6157, 58, 59, 60syl3anbrc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  ( ZZ>= `  ( ( # `  A
)  -  1 ) ) )
62 fzoss2 11892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( ZZ>= `  ( ( # `
 A )  - 
1 ) )  -> 
( 0..^ ( (
# `  A )  -  1 ) ) 
C_  ( 0..^ (
# `  A )
) )
6356, 61, 623syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( 0..^ ( ( # `  A
)  -  1 ) )  C_  ( 0..^ ( # `  A
) ) )
6463sselda 3402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  i  e.  ( 0..^ ( # `  A
) ) )
65643adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  i  e.  ( 0..^ ( # `  A
) ) )
66 swrd0fv 12736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  i )  =  ( B `  i ) )
6754, 55, 65, 66syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  i )  =  ( B `  i ) )
6867eqcomd 2429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( B `  i )  =  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) )
69 elfzom1elp1fzo 11926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  A
)  e.  ZZ  /\  i  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )  ->  (
i  +  1 )  e.  ( 0..^ (
# `  A )
) )
7056, 69sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( # `  A ) ) )
71703adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( # `  A ) ) )
72 swrd0fv 12736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  (
i  +  1 )  e.  ( 0..^ (
# `  A )
) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) )  =  ( B `
 ( i  +  1 ) ) )
7372eqcomd 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4025 . . . . . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . . . . . 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 62 . . . . . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . . . . . 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 2485 . . . . . . . . . . . . . . . . . . . . 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 2796 . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . 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 25508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  e.  C  ->  ( # `
 A )  =  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) )
8382oveq1d 6259 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  e.  C  ->  (
( # `  A )  -  1 )  =  ( ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  -  1 ) )
8483ad2antlr 731 . . . . . . . . . . . . . . . . . . . . 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 6260 . . . . . . . . . . . . . . . . . . . 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 2965 . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . 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 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  =  ( # `  A
)  ->  ( N  e.  Prime 
<->  ( # `  A
)  e.  Prime )
)
8988biimpd 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  =  ( # `  A
)  ->  ( N  e.  Prime  ->  ( # `  A
)  e.  Prime )
)
9089eqcoms 2431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  A )  =  N  ->  ( N  e.  Prime  ->  ( # `  A )  e.  Prime ) )
91 prmnn 14563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  A )  e.  Prime  ->  ( # `  A
)  e.  NN )
92 elfz2nn0 11831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  <-> 
( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) ) )
93 1zzd 10914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
1  e.  ZZ )
94 nn0z 10906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  B )  e.  NN0  ->  ( # `  B
)  e.  ZZ )
9594adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( # `  B )  e.  ZZ )
96 nn0z 10906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  A )  e.  NN0  ->  ( # `  A
)  e.  ZZ )
9796adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( # `  A )  e.  ZZ )
9893, 95, 973jca 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( 1  e.  ZZ  /\  ( # `  B
)  e.  ZZ  /\  ( # `  A )  e.  ZZ ) )
99983adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( 1  e.  ZZ  /\  ( # `
 B )  e.  ZZ  /\  ( # `  A )  e.  ZZ ) )
10099adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( 1  e.  ZZ  /\  ( # `  B )  e.  ZZ  /\  ( # `  A
)  e.  ZZ ) )
101 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( # `  A
)  <_  ( # `  B
) )
102 nnge1 10581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
# `  A )  e.  NN  ->  1  <_  (
# `  A )
)
103101, 102anim12ci 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) )
104100, 103jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
10592, 104sylanb 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  (
( 1  e.  ZZ  /\  ( # `  B
)  e.  ZZ  /\  ( # `  A )  e.  ZZ )  /\  ( 1  <_  ( # `
 A )  /\  ( # `  A )  <_  ( # `  B
) ) ) )
106 elfz2 11737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ( 1 ... ( # `
 B ) )  <-> 
( ( 1  e.  ZZ  /\  ( # `  B )  e.  ZZ  /\  ( # `  A
)  e.  ZZ )  /\  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) ) )
107105, 106sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  ( # `
 A )  e.  ( 1 ... ( # `
 B ) ) )
108 swrd0fvlsw 12740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  ( B `  (
( # `  A )  -  1 ) ) )
109108eqcomd 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B `  (
( # `  A )  -  1 ) )  =  ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) )
110 swrd0fv0 12737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
)  =  ( B `
 0 ) )
111110eqcomd 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B `  0
)  =  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) )
112109, 111preq12d 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  ->  { ( B `  ( ( # `  A
)  -  1 ) ) ,  ( B `
 0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } )
113112expcom 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( 1 ... ( # `
 B ) )  ->  ( B  e. Word  V  ->  { ( B `
 ( ( # `  A )  -  1 ) ) ,  ( B `  0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) ) ,  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
) } ) )
114107, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) } ) )
115114ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) } ) ) )
116115com23 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) } ) ) )
11753, 8, 116sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  C  ->  (
( # `  A )  e.  NN  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
11891, 117syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  A )  e.  Prime  ->  ( c  e.  C  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
11990, 118syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  A )  =  N  ->  ( N  e.  Prime  ->  ( c  e.  C  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) ) )
120119com23 81 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  A )  =  N  ->  ( c  e.  C  ->  ( N  e.  Prime  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) ) )
121120adantl 467 . . . . . . . . . . . . . . . . . . . . . . 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
) } ) ) )
122121imp 430 . . . . . . . . . . . . . . . . . . . . . 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 ) } ) )
123122com12 32 . . . . . . . . . . . . . . . . . . . . 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 ) } ) )
1241233ad2ant3 1028 . . . . . . . . . . . . . . . . . . . 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 ) } ) )
125124impcom 431 . . . . . . . . . . . . . . . . . . 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 ) } )
126125eleq1d 2485 . . . . . . . . . . . . . . . . . 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 ) )
12787, 1263anbi23d 1338 . . . . . . . . . . . . . . . . 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 ) ) )
12852, 127mpbid 213 . . . . . . . . . . . . . . . 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 ) )
129 3simpc 1004 . . . . . . . . . . . . . . . 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 ) )
130128, 129syl 17 . . . . . . . . . . . . . . 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 ) )
131 3anass 986 . . . . . . . . . . . . . . 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 ) ) )
13211, 130, 131sylanbrc 668 . . . . . . . . . . . . . 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 ) )
133 usgrav 25002 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
1341333ad2ant1 1026 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( V  e.  _V  /\  E  e. 
_V ) )
135134adantl 467 . . . . . . . . . . . . . . 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 ) )
136 isclwwlk 25433 . . . . . . . . . . . . . . 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 ) ) )
137135, 136syl 17 . . . . . . . . . . . . . 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 ) ) )
138132, 137mpbird 235 . . . . . . . . . . . . 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 ) )
13982eqeq1d 2425 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  C  ->  (
( # `  A )  =  N  <->  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  =  N ) )
140139biimpcd 227 . . . . . . . . . . . . . . . 16  |-  ( (
# `  A )  =  N  ->  ( c  e.  C  ->  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N ) )
141140adantl 467 . . . . . . . . . . . . . . 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 ) )
142141imp 430 . . . . . . . . . . . . . 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 )
143142adantr 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 ) )  ->  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N )
144138, 143jca 534 . . . . . . . . . . . 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 ) )
145133simpld 460 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  V  e.  _V )
146145adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  V  e. 
_V )
147133simprd 464 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  E  e.  _V )
148147adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  E  e. 
_V )
149 prmnn 14563 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  Prime  ->  N  e.  NN )
150149nnnn0d 10871 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  Prime  ->  N  e. 
NN0 )
151150adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  N  e. 
NN0 )
152146, 148, 1513jca 1185 . . . . . . . . . . . . . . 15  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  ( V  e.  _V  /\  E  e.  _V  /\  N  e. 
NN0 ) )
1531523adant2 1024 . . . . . . . . . . . . . 14  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( V  e.  _V  /\  E  e. 
_V  /\  N  e.  NN0 ) )
154153adantl 467 . . . . . . . . . . . . 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 ) )
155 isclwwlkn 25434 . . . . . . . . . . . . 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 ) ) )
156154, 155syl 17 . . . . . . . . . . . 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 ) ) )
157144, 156mpbird 235 . . . . . . . . . . 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
) )
158157exp31 607 . . . . . . . . . 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 ) ) ) )
159158exp41 613 . . . . . . . . 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 ) ) ) ) ) ) )
1606, 159mpancom 673 . . . . . . . 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 ) ) ) ) ) ) )
161160imp31 433 . . . . . . 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 ) ) ) ) )
1625, 161syl 17 . . . . . 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 ) ) ) ) )
163162imp 430 . . . . 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 ) ) ) )
1642, 163sylbi 198 . . . 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 ) ) ) )
165164pm2.43i 49 . . 3  |-  ( c  e.  C  ->  (
( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) ) )
166165impcom 431 . 2  |-  ( ( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  /\  c  e.  C )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) )
167166, 7fmptd 6000 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   A.wral 2709   {crab 2713   _Vcvv 3017    C_ wss 3374   {cpr 3938   <.cop 3942   class class class wbr 4361    |-> cmpt 4420   dom cdm 4791   ran crn 4792   -->wf 5535   ` cfv 5539  (class class class)co 6244   1stc1st 6744   2ndc2nd 6745   Fincfn 7519   RRcr 9484   0cc0 9485   1c1 9486    + caddc 9488    <_ cle 9622    - cmin 9806   NNcn 10555   2c2 10605   NN0cn0 10815   ZZcz 10883   ZZ>=cuz 11105   ...cfz 11730  ..^cfzo 11861   #chash 12460  Word cword 12599   lastS clsw 12600   substr csubstr 12603   Primecprime 14560   USGrph cusg 24994   ClWalks cclwlk 25412   ClWWalks cclwwlk 25413   ClWWalksN cclwwlkn 25414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-card 8320  df-cda 8544  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-2 10614  df-n0 10816  df-z 10884  df-uz 11106  df-fz 11731  df-fzo 11862  df-hash 12461  df-word 12607  df-lsw 12608  df-substr 12611  df-dvds 14244  df-prm 14561  df-usgra 24997  df-wlk 25173  df-clwlk 25415  df-clwwlk 25416  df-clwwlkn 25417
This theorem is referenced by:  clwlkfoclwwlk  25510  clwlkf1clwwlk  25515
  Copyright terms: Public domain W3C validator