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

Theorem clwlkfclwwlk 24970
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 3106 . . . . 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 24890 . . . . . . 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 12568 . . . . . . . . 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 24966 . . . . . . . . . . . . . . . . 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 12654 . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . 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 14246 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  Prime  ->  N  e.  ( ZZ>= `  2 )
)
17 hashfzdm 12501 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  A )  e.  ( ZZ>= `  2 )  <->  ( 2  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  2  <_  ( # `  A
) ) )
20 2re 10626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  2  e.  RR
2120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  2  e.  RR )
22 zre 10889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  RR )
23 peano2re 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
# `  A )  e.  RR  ->  ( ( # `
 A )  +  1 )  e.  RR )
2422, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  +  1 )  e.  RR )
2521, 22, 243jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  <_  ( ( # `
 A )  +  1 ) )
2928adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  ( # `
 A )  <_ 
( ( # `  A
)  +  1 ) )
30 letr 9695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( # `  A
)  e.  ZZ  /\  2  <_  ( # `  A
) )  ->  2  <_  ( ( # `  A
)  +  1 ) )
33323adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  =  ( # `  A
)  ->  ( N  e.  ( ZZ>= `  2 )  <->  (
# `  A )  e.  ( ZZ>= `  2 )
) )
3736eqcoms 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4460 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1019 . . . . . . . . . . . . . . . . . . 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 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 ) )  ->  ( A. i  e.  (
0..^ ( # `  A
) ) ( E `
 ( A `  i ) )  =  { ( B `  i ) ,  ( B `  ( i  +  1 ) ) }  /\  ( B `
 0 )  =  ( B `  ( # `
 A ) ) ) )
51 clwlkisclwwlklem1 24913 . . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . . 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 24968 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  e.  C  ->  ( # `
 A )  e.  ( 0 ... ( # `
 B ) ) )
54 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  B  e. Word  V )
55 simp1 996 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( # `  A
)  e.  ( 0 ... ( # `  B
) ) )
56 elfzelz 11713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  ->  ( # `  A
)  e.  ZZ )
57 peano2zm 10928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  - 
1 )  e.  ZZ )
58 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  ZZ )
5922lem1d 10499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ZZ  ->  ( ( # `
 A )  - 
1 )  <_  ( # `
 A ) )
60 eluz2 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ( ZZ>= `  ( ( # `
 A )  - 
1 ) )  <->  ( (
( # `  A )  -  1 )  e.  ZZ  /\  ( # `  A )  e.  ZZ  /\  ( ( # `  A
)  -  1 )  <_  ( # `  A
) ) )
6157, 58, 59, 60syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
# `  A )  e.  ZZ  ->  ( # `  A
)  e.  ( ZZ>= `  ( ( # `  A
)  -  1 ) ) )
62 fzoss2 11851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  i  e.  ( 0..^ ( # `  A
) ) )
65643adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  i  e.  ( 0..^ ( # `  A
) ) )
66 swrd0fv 12674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( ( B substr  <. 0 ,  ( # `  A ) >. ) `  i )  =  ( B `  i ) )
6754, 55, 65, 66syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  i )  =  ( B `  i ) )
6867eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( B `  i )  =  ( ( B substr  <. 0 ,  ( # `  A
) >. ) `  i
) )
69 elfzom1elp1fzo 11885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  B  e. Word  V  /\  i  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( # `  A ) ) )
72 swrd0fv 12674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 0 ... ( # `  B
) )  /\  (
i  +  1 )  e.  ( 0..^ (
# `  A )
) )  ->  (
( B substr  <. 0 ,  ( # `  A
) >. ) `  (
i  +  1 ) )  =  ( B `
 ( i  +  1 ) ) )
7372eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4119 . . . . . . . . . . . . . . . . . . . . . . . . 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 1195 . . . . . . . . . . . . . . . . . . . . . . . 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 2526 . . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . . 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 24969 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  e.  C  ->  ( # `
 A )  =  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) )
8382oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . . . 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 3060 . . . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  =  ( # `  A
)  ->  ( N  e.  Prime 
<->  ( # `  A
)  e.  Prime )
)
8988biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  =  ( # `  A
)  ->  ( N  e.  Prime  ->  ( # `  A
)  e.  Prime )
)
9089eqcoms 2469 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  A )  =  N  ->  ( N  e.  Prime  ->  ( # `  A )  e.  Prime ) )
91 prmnn 14231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  A )  e.  Prime  ->  ( # `  A
)  e.  NN )
92 elfz2nn0 11794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
# `  A )  e.  ( 0 ... ( # `
 B ) )  <-> 
( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) ) )
93 1zzd 10916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
1  e.  ZZ )
94 nn0z 10908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  B )  e.  NN0  ->  ( # `  B
)  e.  ZZ )
9594adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( # `  B )  e.  ZZ )
96 nn0z 10908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  A )  e.  NN0  ->  ( # `  A
)  e.  ZZ )
9796adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( # `  A )  e.  ZZ )
9893, 95, 973jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0 )  -> 
( 1  e.  ZZ  /\  ( # `  B
)  e.  ZZ  /\  ( # `  A )  e.  ZZ ) )
99983adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( 1  e.  ZZ  /\  ( # `
 B )  e.  ZZ  /\  ( # `  A )  e.  ZZ ) )
10099adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( 1  e.  ZZ  /\  ( # `  B )  e.  ZZ  /\  ( # `  A
)  e.  ZZ ) )
101 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( # `  A
)  <_  ( # `  B
) )
102 nnge1 10582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
# `  A )  e.  NN  ->  1  <_  (
# `  A )
)
103101, 102anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  /\  ( # `  A )  e.  NN )  ->  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) )
104100, 103jca 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
) ) ) )
10592, 104sylanb 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  (
( 1  e.  ZZ  /\  ( # `  B
)  e.  ZZ  /\  ( # `  A )  e.  ZZ )  /\  ( 1  <_  ( # `
 A )  /\  ( # `  A )  <_  ( # `  B
) ) ) )
106 elfz2 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
# `  A )  e.  ( 1 ... ( # `
 B ) )  <-> 
( ( 1  e.  ZZ  /\  ( # `  B )  e.  ZZ  /\  ( # `  A
)  e.  ZZ )  /\  ( 1  <_ 
( # `  A )  /\  ( # `  A
)  <_  ( # `  B
) ) ) )
107105, 106sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( # `  A
)  e.  ( 0 ... ( # `  B
) )  /\  ( # `
 A )  e.  NN )  ->  ( # `
 A )  e.  ( 1 ... ( # `
 B ) ) )
108 swrd0fvlsw 12678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( lastS  `  ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  ( B `  (
( # `  A )  -  1 ) ) )
109108eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B `  (
( # `  A )  -  1 ) )  =  ( lastS  `  ( B substr  <. 0 ,  (
# `  A ) >. ) ) )
110 swrd0fv0 12675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( ( B substr  <. 0 ,  ( # `  A
) >. ) `  0
)  =  ( B `
 0 ) )
111110eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( B  e. Word  V  /\  ( # `  A )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B `  0
)  =  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) )
112109, 111preq12d 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) } ) )
114107, 113syl 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 ) } ) )
115114ex 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
) } ) ) )
116115com23 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
) } ) ) )
11753, 8, 116sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  C  ->  (
( # `  A )  e.  NN  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
11891, 117syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
# `  A )  e.  Prime  ->  ( c  e.  C  ->  { ( B `  ( (
# `  A )  -  1 ) ) ,  ( B ` 
0 ) }  =  { ( lastS  `  ( B substr  <. 0 ,  ( # `  A ) >. )
) ,  ( ( B substr  <. 0 ,  (
# `  A ) >. ) `  0 ) } ) )
11990, 118syl6 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 ) } ) ) )
120119com23 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 ) } ) ) )
121120adantl 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
) } ) ) )
122121imp 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 ) } ) )
123122com12 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 ) } ) )
1241233ad2ant3 1019 . . . . . . . . . . . . . . . . . . . 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 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 ) } )
126125eleq1d 2526 . . . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . . . 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 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 ) )
129 3simpc 995 . . . . . . . . . . . . . . . 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 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 ) )
131 3anass 977 . . . . . . . . . . . . . . 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 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 ) )
133 usgrav 24464 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
1341333ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( V  e.  _V  /\  E  e. 
_V ) )
135134adantl 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 ) )
136 isclwwlk 24894 . . . . . . . . . . . . . . 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 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 ) ) )
138132, 137mpbird 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 ) )
13982eqeq1d 2459 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  C  ->  (
( # `  A )  =  N  <->  ( # `  ( B substr  <. 0 ,  (
# `  A ) >. ) )  =  N ) )
140139biimpcd 224 . . . . . . . . . . . . . . . 16  |-  ( (
# `  A )  =  N  ->  ( c  e.  C  ->  ( # `
 ( B substr  <. 0 ,  ( # `  A
) >. ) )  =  N ) )
141140adantl 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 ) )
142141imp 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 )
143142adantr 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 )
144138, 143jca 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 ) )
145133simpld 459 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  V  e.  _V )
146145adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  V  e. 
_V )
147133simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( V USGrph  E  ->  E  e.  _V )
148147adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  E  e. 
_V )
149 prmnn 14231 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  Prime  ->  N  e.  NN )
150149nnnn0d 10873 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  Prime  ->  N  e. 
NN0 )
151150adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  N  e. 
NN0 )
152146, 148, 1513jca 1176 . . . . . . . . . . . . . . 15  |-  ( ( V USGrph  E  /\  N  e. 
Prime )  ->  ( V  e.  _V  /\  E  e.  _V  /\  N  e. 
NN0 ) )
1531523adant2 1015 . . . . . . . . . . . . . 14  |-  ( ( V USGrph  E  /\  V  e. 
Fin  /\  N  e.  Prime )  ->  ( V  e.  _V  /\  E  e. 
_V  /\  N  e.  NN0 ) )
154153adantl 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 ) )
155 isclwwlkn 24895 . . . . . . . . . . . . 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 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 ) ) )
157144, 156mpbird 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
) )
158157exp31 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 ) ) ) )
159158exp41 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 ) ) ) ) ) ) )
1606, 159mpancom 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 ) ) ) ) ) ) )
161160imp31 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 ) ) ) ) )
1625, 161syl 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 ) ) ) ) )
163162imp 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 ) ) ) )
1642, 163sylbi 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 ) ) ) )
165164pm2.43i 47 . . 3  |-  ( c  e.  C  ->  (
( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) ) )
166165impcom 430 . 2  |-  ( ( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  Prime )  /\  c  e.  C )  ->  ( B substr  <. 0 ,  (
# `  A ) >. )  e.  ( ( V ClWWalksN  E ) `  N
) )
167166, 7fmptd 6056 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 973    = wceq 1395    e. wcel 1819   A.wral 2807   {crab 2811   _Vcvv 3109    C_ wss 3471   {cpr 4034   <.cop 4038   class class class wbr 4456    |-> cmpt 4515   dom cdm 5008   ran crn 5009   -->wf 5590   ` cfv 5594  (class class class)co 6296   1stc1st 6797   2ndc2nd 6798   Fincfn 7535   RRcr 9508   0cc0 9509   1c1 9510    + caddc 9512    <_ cle 9646    - cmin 9824   NNcn 10556   2c2 10606   NN0cn0 10816   ZZcz 10885   ZZ>=cuz 11106   ...cfz 11697  ..^cfzo 11820   #chash 12407  Word cword 12537   lastS clsw 12538   substr csubstr 12541   Primecprime 14228   USGrph cusg 24456   ClWalks cclwlk 24873   ClWWalks cclwwlk 24874   ClWWalksN cclwwlkn 24875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-n0 10817  df-z 10886  df-uz 11107  df-fz 11698  df-fzo 11821  df-hash 12408  df-word 12545  df-lsw 12546  df-substr 12549  df-dvds 13998  df-prm 14229  df-usgra 24459  df-wlk 24634  df-clwlk 24876  df-clwwlk 24877  df-clwwlkn 24878
This theorem is referenced by:  clwlkfoclwwlk  24971  clwlkf1clwwlk  24976
  Copyright terms: Public domain W3C validator