This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwlkinwwlk

Description: If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 23-Jan-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Assertion clwwlkinwwlk 
|- ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ W e. ( M WWalksN G ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( W prefix N ) e. ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 wwlknp 
 |-  ( W e. ( M WWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
4 pfxcl 
 |-  ( W e. Word ( Vtx ` G ) -> ( W prefix N ) e. Word ( Vtx ` G ) )
5 4 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) -> ( W prefix N ) e. Word ( Vtx ` G ) )
6 5 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( W prefix N ) e. Word ( Vtx ` G ) )
7 simpll 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> W e. Word ( Vtx ` G ) )
8 simprl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. NN )
9 eluz2 
 |-  ( M e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ M e. ZZ /\ N <_ M ) )
10 zre 
 |-  ( N e. ZZ -> N e. RR )
11 zre 
 |-  ( M e. ZZ -> M e. RR )
12 id 
 |-  ( N <_ M -> N <_ M )
13 10 11 12 3anim123i 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ N <_ M ) -> ( N e. RR /\ M e. RR /\ N <_ M ) )
14 9 13 sylbi 
 |-  ( M e. ( ZZ>= ` N ) -> ( N e. RR /\ M e. RR /\ N <_ M ) )
15 letrp1 
 |-  ( ( N e. RR /\ M e. RR /\ N <_ M ) -> N <_ ( M + 1 ) )
16 14 15 syl 
 |-  ( M e. ( ZZ>= ` N ) -> N <_ ( M + 1 ) )
17 16 adantl 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> N <_ ( M + 1 ) )
18 17 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N <_ ( M + 1 ) )
19 breq2 
 |-  ( ( # ` W ) = ( M + 1 ) -> ( N <_ ( # ` W ) <-> N <_ ( M + 1 ) ) )
20 19 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( N <_ ( # ` W ) <-> N <_ ( M + 1 ) ) )
21 18 20 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N <_ ( # ` W ) )
22 pfxn0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. NN /\ N <_ ( # ` W ) ) -> ( W prefix N ) =/= (/) )
23 7 8 21 22 syl3anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( W prefix N ) =/= (/) )
24 6 23 jca 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) )
25 24 3adantl3 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) )
26 25 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) )
27 nnz 
 |-  ( N e. NN -> N e. ZZ )
28 1nn0 
 |-  1 e. NN0
29 eluzmn 
 |-  ( ( N e. ZZ /\ 1 e. NN0 ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
30 27 28 29 sylancl 
 |-  ( N e. NN -> N e. ( ZZ>= ` ( N - 1 ) ) )
31 uzss 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` ( N - 1 ) ) )
32 30 31 syl 
 |-  ( N e. NN -> ( ZZ>= ` N ) C_ ( ZZ>= ` ( N - 1 ) ) )
33 32 sselda 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` ( N - 1 ) ) )
34 fzoss2 
 |-  ( M e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ M ) )
35 33 34 syl 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ M ) )
36 35 3ad2ant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ M ) )
37 ssralv 
 |-  ( ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ M ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
38 36 37 syl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
39 38 3exp 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( M + 1 ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
40 39 com34 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( M + 1 ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
41 40 3imp1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) )
42 41 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) )
43 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
44 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
45 43 44 sylib 
 |-  ( N e. NN -> N e. ( ZZ>= ` 0 ) )
46 eluzfz 
 |-  ( ( N e. ( ZZ>= ` 0 ) /\ M e. ( ZZ>= ` N ) ) -> N e. ( 0 ... M ) )
47 45 46 sylan 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> N e. ( 0 ... M ) )
48 fzelp1 
 |-  ( N e. ( 0 ... M ) -> N e. ( 0 ... ( M + 1 ) ) )
49 47 48 syl 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> N e. ( 0 ... ( M + 1 ) ) )
50 49 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 0 ... ( M + 1 ) ) )
51 oveq2 
 |-  ( ( # ` W ) = ( M + 1 ) -> ( 0 ... ( # ` W ) ) = ( 0 ... ( M + 1 ) ) )
52 51 eleq2d 
 |-  ( ( # ` W ) = ( M + 1 ) -> ( N e. ( 0 ... ( # ` W ) ) <-> N e. ( 0 ... ( M + 1 ) ) ) )
53 52 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( N e. ( 0 ... ( # ` W ) ) <-> N e. ( 0 ... ( M + 1 ) ) ) )
54 50 53 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
55 pfxlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix N ) ) = N )
56 7 54 55 syl2anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( # ` ( W prefix N ) ) = N )
57 56 oveq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( ( # ` ( W prefix N ) ) - 1 ) = ( N - 1 ) )
58 57 oveq2d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) = ( 0 ..^ ( N - 1 ) ) )
59 58 raleqdv 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
60 7 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> W e. Word ( Vtx ` G ) )
61 54 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
62 30 ad2antrl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
63 fzoss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
64 62 63 syl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
65 64 sselda 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i e. ( 0 ..^ N ) )
66 pfxfv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W prefix N ) ` i ) = ( W ` i ) )
67 60 61 65 66 syl3anc 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( W prefix N ) ` i ) = ( W ` i ) )
68 27 ad2antrl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ZZ )
69 elfzom1elp1fzo 
 |-  ( ( N e. ZZ /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ N ) )
70 68 69 sylan 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ N ) )
71 pfxfv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) /\ ( i + 1 ) e. ( 0 ..^ N ) ) -> ( ( W prefix N ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
72 60 61 70 71 syl3anc 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( W prefix N ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
73 67 72 preq12d 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
74 73 eleq1d 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
75 74 ralbidva 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
76 59 75 bitrd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
77 76 3adantl3 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
78 77 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
79 42 78 mpbird 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
80 elfz1uz 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> N e. ( 1 ... M ) )
81 fzelp1 
 |-  ( N e. ( 1 ... M ) -> N e. ( 1 ... ( M + 1 ) ) )
82 80 81 syl 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> N e. ( 1 ... ( M + 1 ) ) )
83 82 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 1 ... ( M + 1 ) ) )
84 oveq2 
 |-  ( ( # ` W ) = ( M + 1 ) -> ( 1 ... ( # ` W ) ) = ( 1 ... ( M + 1 ) ) )
85 84 eleq2d 
 |-  ( ( # ` W ) = ( M + 1 ) -> ( N e. ( 1 ... ( # ` W ) ) <-> N e. ( 1 ... ( M + 1 ) ) ) )
86 85 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( N e. ( 1 ... ( # ` W ) ) <-> N e. ( 1 ... ( M + 1 ) ) ) )
87 83 86 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 1 ... ( # ` W ) ) )
88 pfxfvlsw 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix N ) ) = ( W ` ( N - 1 ) ) )
89 pfxfv0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix N ) ` 0 ) = ( W ` 0 ) )
90 88 89 preq12d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` W ) ) ) -> { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
91 7 87 90 syl2anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
92 91 3adantl3 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
93 92 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
94 fz1fzo0m1 
 |-  ( N e. ( 1 ... M ) -> ( N - 1 ) e. ( 0 ..^ M ) )
95 80 94 syl 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( N - 1 ) e. ( 0 ..^ M ) )
96 95 3ad2ant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( N - 1 ) e. ( 0 ..^ M ) )
97 simpr 
 |-  ( ( N e. NN /\ i = ( N - 1 ) ) -> i = ( N - 1 ) )
98 97 fveq2d 
 |-  ( ( N e. NN /\ i = ( N - 1 ) ) -> ( W ` i ) = ( W ` ( N - 1 ) ) )
99 oveq1 
 |-  ( i = ( N - 1 ) -> ( i + 1 ) = ( ( N - 1 ) + 1 ) )
100 nncn 
 |-  ( N e. NN -> N e. CC )
101 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
102 100 101 syl 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
103 99 102 sylan9eqr 
 |-  ( ( N e. NN /\ i = ( N - 1 ) ) -> ( i + 1 ) = N )
104 103 fveq2d 
 |-  ( ( N e. NN /\ i = ( N - 1 ) ) -> ( W ` ( i + 1 ) ) = ( W ` N ) )
105 98 104 preq12d 
 |-  ( ( N e. NN /\ i = ( N - 1 ) ) -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } )
106 105 eleq1d 
 |-  ( ( N e. NN /\ i = ( N - 1 ) ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) )
107 106 ex 
 |-  ( N e. NN -> ( i = ( N - 1 ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) )
108 107 adantr 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( i = ( N - 1 ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) )
109 108 3ad2ant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( i = ( N - 1 ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) )
110 109 imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ i = ( N - 1 ) ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) )
111 96 110 rspcdv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) )
112 111 3exp 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( M + 1 ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) ) )
113 112 com34 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( M + 1 ) -> ( A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) ) )
114 113 3imp1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) )
115 114 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) )
116 preq2 
 |-  ( ( W ` N ) = ( W ` 0 ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
117 116 eleq1d 
 |-  ( ( W ` N ) = ( W ` 0 ) -> ( { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
118 117 adantl 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
119 115 118 mpbid 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) )
120 93 119 eqeltrd 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } e. ( Edg ` G ) )
121 26 79 120 3jca 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } e. ( Edg ` G ) ) )
122 121 exp31 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( ( W ` N ) = ( W ` 0 ) -> ( ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } e. ( Edg ` G ) ) ) ) )
123 122 3imp21 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } e. ( Edg ` G ) ) )
124 1 2 isclwwlk 
 |-  ( ( W prefix N ) e. ( ClWWalks ` G ) <-> ( ( ( W prefix N ) e. Word ( Vtx ` G ) /\ ( W prefix N ) =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` ( W prefix N ) ) - 1 ) ) { ( ( W prefix N ) ` i ) , ( ( W prefix N ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W prefix N ) ) , ( ( W prefix N ) ` 0 ) } e. ( Edg ` G ) ) )
125 123 124 sylibr 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( W prefix N ) e. ( ClWWalks ` G ) )
126 47 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 0 ... M ) )
127 126 48 syl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 0 ... ( M + 1 ) ) )
128 127 53 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
129 7 128 jca 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) /\ ( N e. NN /\ M e. ( ZZ>= ` N ) ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) )
130 129 ex 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) )
131 130 3adant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) )
132 131 impcom 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) )
133 132 3adant3 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) )
134 133 55 syl 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( # ` ( W prefix N ) ) = N )
135 isclwwlkn 
 |-  ( ( W prefix N ) e. ( N ClWWalksN G ) <-> ( ( W prefix N ) e. ( ClWWalks ` G ) /\ ( # ` ( W prefix N ) ) = N ) )
136 125 134 135 sylanbrc 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( M + 1 ) /\ A. i e. ( 0 ..^ M ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( W prefix N ) e. ( N ClWWalksN G ) )
137 3 136 syl3an2 
 |-  ( ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) /\ W e. ( M WWalksN G ) /\ ( W ` N ) = ( W ` 0 ) ) -> ( W prefix N ) e. ( N ClWWalksN G ) )