Metamath Proof Explorer

Theorem clwwlkwwlksb

Description: A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022)

Ref Expression
Hypothesis clwwlkwwlksb.v 
|- V = ( Vtx ` G )
Assertion clwwlkwwlksb 
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkwwlksb.v 
 |-  V = ( Vtx ` G )
2 fstwrdne 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )
3 2 s1cld 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> <" ( W ` 0 ) "> e. Word V )
4 ccatlen 
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) )
5 3 4 syldan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) )
6 s1len 
 |-  ( # ` <" ( W ` 0 ) "> ) = 1
7 6 oveq2i 
 |-  ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + 1 )
8 5 7 eqtrdi 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + 1 ) )
9 8 oveq1d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) = ( ( ( # ` W ) + 1 ) - 1 ) )
10 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
11 10 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
12 11 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. CC )
13 1cnd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> 1 e. CC )
14 12 13 13 addsubd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( ( ( # ` W ) - 1 ) + 1 ) )
15 9 14 eqtrd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) = ( ( ( # ` W ) - 1 ) + 1 ) )
16 15 oveq2d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) = ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) )
17 16 raleqdv 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
18 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
19 nnm1nn0 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
20 18 19 syl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. NN0 )
21 elnn0uz 
 |-  ( ( ( # ` W ) - 1 ) e. NN0 <-> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
22 20 21 sylib 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
23 fzosplitsn 
 |-  ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) )
24 22 23 syl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) )
25 24 raleqdv 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
26 ralunb 
 |-  ( A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
27 25 26 bitrdi 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
28 simpl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> W e. Word V )
29 10 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
30 29 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. ZZ )
31 elfzom1elfzo 
 |-  ( ( ( # ` W ) e. ZZ /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
32 30 31 sylan 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
33 ccats1val1 
 |-  ( ( W e. Word V /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` i ) = ( W ` i ) )
34 28 32 33 syl2an2r 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` i ) = ( W ` i ) )
35 elfzom1elp1fzo 
 |-  ( ( ( # ` W ) e. ZZ /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) )
36 30 35 sylan 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) )
37 ccats1val1 
 |-  ( ( W e. Word V /\ ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
38 28 36 37 syl2an2r 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
39 34 38 preq12d 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
40 39 eleq1d 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
41 40 ralbidva 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
42 ovex 
 |-  ( ( # ` W ) - 1 ) e. _V
43 fveq2 
 |-  ( i = ( ( # ` W ) - 1 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` i ) = ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) )
44 fvoveq1 
 |-  ( i = ( ( # ` W ) - 1 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) = ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) )
45 43 44 preq12d 
 |-  ( i = ( ( # ` W ) - 1 ) -> { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } = { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } )
46 45 eleq1d 
 |-  ( i = ( ( # ` W ) - 1 ) -> ( { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
47 42 46 ralsn 
 |-  ( A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. ( Edg ` G ) )
48 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
49 18 48 syl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
50 ccats1val1 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
51 49 50 syldan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
52 lsw 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
53 52 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
54 51 53 eqtr4d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
55 npcan1 
 |-  ( ( # ` W ) e. CC -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
56 11 55 syl 
 |-  ( W e. Word V -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
57 56 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
58 57 fveq2d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( W ++ <" ( W ` 0 ) "> ) ` ( # ` W ) ) )
59 eqidd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) = ( # ` W ) )
60 ccats1val2 
 |-  ( ( W e. Word V /\ ( W ` 0 ) e. V /\ ( # ` W ) = ( # ` W ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( # ` W ) ) = ( W ` 0 ) )
61 28 2 59 60 syl3anc 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( # ` W ) ) = ( W ` 0 ) )
62 58 61 eqtrd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( W ` 0 ) )
63 54 62 preq12d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } = { ( lastS ` W ) , ( W ` 0 ) } )
64 63 eleq1d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. ( Edg ` G ) <-> { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
65 47 64 bitrid 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
66 41 65 anbi12d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
67 17 27 66 3bitrd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
68 28 3 jca 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) )
69 ccat0 
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( ( W ++ <" ( W ` 0 ) "> ) = (/) <-> ( W = (/) /\ <" ( W ` 0 ) "> = (/) ) ) )
70 simpl 
 |-  ( ( W = (/) /\ <" ( W ` 0 ) "> = (/) ) -> W = (/) )
71 69 70 biimtrdi 
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( ( W ++ <" ( W ` 0 ) "> ) = (/) -> W = (/) ) )
72 71 necon3d 
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( W =/= (/) -> ( W ++ <" ( W ` 0 ) "> ) =/= (/) ) )
73 72 adantld 
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( ( W e. Word V /\ W =/= (/) ) -> ( W ++ <" ( W ` 0 ) "> ) =/= (/) ) )
74 68 73 mpcom 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ++ <" ( W ` 0 ) "> ) =/= (/) )
75 wrdv 
 |-  ( W e. Word V -> W e. Word _V )
76 s1cli 
 |-  <" ( W ` 0 ) "> e. Word _V
77 ccatalpha 
 |-  ( ( W e. Word _V /\ <" ( W ` 0 ) "> e. Word _V ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. Word V <-> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) ) )
78 75 76 77 sylancl 
 |-  ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) e. Word V <-> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) ) )
79 78 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. Word V <-> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) ) )
80 28 3 79 mpbir2and 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ++ <" ( W ` 0 ) "> ) e. Word V )
81 74 80 jca 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) )
82 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
83 1 82 iswwlks 
 |-  ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
84 df-3an 
 |-  ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
85 83 84 bitri 
 |-  ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
86 85 a1i 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
87 81 86 mpbirand 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
88 1 82 isclwwlk 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
89 3anass 
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
90 88 89 bitri 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
91 90 baib 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
92 67 87 91 3bitr4rd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) )