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

Metamath Proof Explorer

Theorem clwwlkext2edg

Description: If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses clwwlkext2edg.v 
|- V = ( Vtx ` G )
clwwlkext2edg.e 
|- E = ( Edg ` G )
Assertion clwwlkext2edg 
|- ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" Z "> ) e. ( N ClWWalksN G ) ) -> ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) )

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v 
 |-  V = ( Vtx ` G )
2 clwwlkext2edg.e 
 |-  E = ( Edg ` G )
3 clwwlknnn 
 |-  ( ( W ++ <" Z "> ) e. ( N ClWWalksN G ) -> N e. NN )
4 1 2 isclwwlknx 
 |-  ( N e. NN -> ( ( W ++ <" Z "> ) e. ( N ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) ) )
5 ige2m2fzo 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) )
6 5 3ad2ant3 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) )
7 6 adantr 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) )
8 oveq1 
 |-  ( ( # ` ( W ++ <" Z "> ) ) = N -> ( ( # ` ( W ++ <" Z "> ) ) - 1 ) = ( N - 1 ) )
9 8 oveq2d 
 |-  ( ( # ` ( W ++ <" Z "> ) ) = N -> ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) = ( 0 ..^ ( N - 1 ) ) )
10 9 eleq2d 
 |-  ( ( # ` ( W ++ <" Z "> ) ) = N -> ( ( N - 2 ) e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) <-> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) ) )
11 10 adantl 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( N - 2 ) e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) <-> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) ) )
12 7 11 mpbird 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( N - 2 ) e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) )
13 fveq2 
 |-  ( i = ( N - 2 ) -> ( ( W ++ <" Z "> ) ` i ) = ( ( W ++ <" Z "> ) ` ( N - 2 ) ) )
14 fvoveq1 
 |-  ( i = ( N - 2 ) -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) )
15 13 14 preq12d 
 |-  ( i = ( N - 2 ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( ( W ++ <" Z "> ) ` ( N - 2 ) ) , ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) } )
16 15 eleq1d 
 |-  ( i = ( N - 2 ) -> ( { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` ( N - 2 ) ) , ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) } e. E ) )
17 16 rspcv 
 |-  ( ( N - 2 ) e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E -> { ( ( W ++ <" Z "> ) ` ( N - 2 ) ) , ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) } e. E ) )
18 12 17 syl 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E -> { ( ( W ++ <" Z "> ) ` ( N - 2 ) ) , ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) } e. E ) )
19 wrdlenccats1lenm1 
 |-  ( W e. Word V -> ( ( # ` ( W ++ <" Z "> ) ) - 1 ) = ( # ` W ) )
20 19 eqcomd 
 |-  ( W e. Word V -> ( # ` W ) = ( ( # ` ( W ++ <" Z "> ) ) - 1 ) )
21 20 adantr 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( # ` W ) = ( ( # ` ( W ++ <" Z "> ) ) - 1 ) )
22 21 8 sylan9eq 
 |-  ( ( ( W e. Word V /\ Z e. V ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( # ` W ) = ( N - 1 ) )
23 22 ex 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( # ` W ) = ( N - 1 ) ) )
24 23 3adant3 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( # ` W ) = ( N - 1 ) ) )
25 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
26 1cnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. CC )
27 25 26 26 subsub4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N - 1 ) - 1 ) = ( N - ( 1 + 1 ) ) )
28 1p1e2 
 |-  ( 1 + 1 ) = 2
29 28 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 + 1 ) = 2 )
30 29 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - ( 1 + 1 ) ) = ( N - 2 ) )
31 27 30 eqtr2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) = ( ( N - 1 ) - 1 ) )
32 31 3ad2ant3 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 2 ) = ( ( N - 1 ) - 1 ) )
33 oveq1 
 |-  ( ( # ` W ) = ( N - 1 ) -> ( ( # ` W ) - 1 ) = ( ( N - 1 ) - 1 ) )
34 33 eqcomd 
 |-  ( ( # ` W ) = ( N - 1 ) -> ( ( N - 1 ) - 1 ) = ( ( # ` W ) - 1 ) )
35 32 34 sylan9eq 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( N - 2 ) = ( ( # ` W ) - 1 ) )
36 35 ex 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` W ) = ( N - 1 ) -> ( N - 2 ) = ( ( # ` W ) - 1 ) ) )
37 24 36 syld 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( N - 2 ) = ( ( # ` W ) - 1 ) ) )
38 37 imp 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( N - 2 ) = ( ( # ` W ) - 1 ) )
39 38 fveq2d 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W ++ <" Z "> ) ` ( N - 2 ) ) = ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) )
40 simpl1 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> W e. Word V )
41 s1cl 
 |-  ( Z e. V -> <" Z "> e. Word V )
42 41 3ad2ant2 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> <" Z "> e. Word V )
43 42 adantr 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> <" Z "> e. Word V )
44 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
45 zre 
 |-  ( N e. ZZ -> N e. RR )
46 1red 
 |-  ( ( N e. RR /\ 2 <_ N ) -> 1 e. RR )
47 2re 
 |-  2 e. RR
48 47 a1i 
 |-  ( ( N e. RR /\ 2 <_ N ) -> 2 e. RR )
49 simpl 
 |-  ( ( N e. RR /\ 2 <_ N ) -> N e. RR )
50 1lt2 
 |-  1 < 2
51 50 a1i 
 |-  ( ( N e. RR /\ 2 <_ N ) -> 1 < 2 )
52 simpr 
 |-  ( ( N e. RR /\ 2 <_ N ) -> 2 <_ N )
53 46 48 49 51 52 ltletrd 
 |-  ( ( N e. RR /\ 2 <_ N ) -> 1 < N )
54 1red 
 |-  ( N e. RR -> 1 e. RR )
55 id 
 |-  ( N e. RR -> N e. RR )
56 54 55 posdifd 
 |-  ( N e. RR -> ( 1 < N <-> 0 < ( N - 1 ) ) )
57 56 adantr 
 |-  ( ( N e. RR /\ 2 <_ N ) -> ( 1 < N <-> 0 < ( N - 1 ) ) )
58 53 57 mpbid 
 |-  ( ( N e. RR /\ 2 <_ N ) -> 0 < ( N - 1 ) )
59 58 ex 
 |-  ( N e. RR -> ( 2 <_ N -> 0 < ( N - 1 ) ) )
60 45 59 syl 
 |-  ( N e. ZZ -> ( 2 <_ N -> 0 < ( N - 1 ) ) )
61 60 a1i 
 |-  ( 2 e. ZZ -> ( N e. ZZ -> ( 2 <_ N -> 0 < ( N - 1 ) ) ) )
62 61 3imp 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> 0 < ( N - 1 ) )
63 44 62 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 < ( N - 1 ) )
64 63 ad2antlr 
 |-  ( ( ( W e. Word V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> 0 < ( N - 1 ) )
65 breq2 
 |-  ( ( # ` W ) = ( N - 1 ) -> ( 0 < ( # ` W ) <-> 0 < ( N - 1 ) ) )
66 65 adantl 
 |-  ( ( ( W e. Word V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N - 1 ) ) )
67 64 66 mpbird 
 |-  ( ( ( W e. Word V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> 0 < ( # ` W ) )
68 hashneq0 
 |-  ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
69 68 adantr 
 |-  ( ( W e. Word V /\ N e. ( ZZ>= ` 2 ) ) -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
70 69 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
71 67 70 mpbid 
 |-  ( ( ( W e. Word V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> W =/= (/) )
72 71 3adantl2 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> W =/= (/) )
73 40 43 72 3jca 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) )
74 73 ex 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` W ) = ( N - 1 ) -> ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) ) )
75 24 74 syld 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) ) )
76 75 imp 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) )
77 ccatval1lsw 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
78 76 77 syl 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
79 39 78 eqtrd 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W ++ <" Z "> ) ` ( N - 2 ) ) = ( lastS ` W ) )
80 2m1e1 
 |-  ( 2 - 1 ) = 1
81 80 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 - 1 ) = 1 )
82 81 eqcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 = ( 2 - 1 ) )
83 82 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) = ( N - ( 2 - 1 ) ) )
84 2cnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. CC )
85 25 84 26 subsubd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - ( 2 - 1 ) ) = ( ( N - 2 ) + 1 ) )
86 83 85 eqtr2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
87 86 3ad2ant3 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
88 eqeq2 
 |-  ( ( # ` W ) = ( N - 1 ) -> ( ( ( N - 2 ) + 1 ) = ( # ` W ) <-> ( ( N - 2 ) + 1 ) = ( N - 1 ) ) )
89 87 88 syl5ibrcom 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` W ) = ( N - 1 ) -> ( ( N - 2 ) + 1 ) = ( # ` W ) ) )
90 24 89 syld 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( ( N - 2 ) + 1 ) = ( # ` W ) ) )
91 90 imp 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( N - 2 ) + 1 ) = ( # ` W ) )
92 91 fveq2d 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) = ( ( W ++ <" Z "> ) ` ( # ` W ) ) )
93 id 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( W e. Word V /\ Z e. V ) )
94 93 3adant3 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( W e. Word V /\ Z e. V ) )
95 94 adantr 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( W e. Word V /\ Z e. V ) )
96 ccatws1ls 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = Z )
97 95 96 syl 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = Z )
98 92 97 eqtrd 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) = Z )
99 79 98 preq12d 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> { ( ( W ++ <" Z "> ) ` ( N - 2 ) ) , ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) } = { ( lastS ` W ) , Z } )
100 99 eleq1d 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( { ( ( W ++ <" Z "> ) ` ( N - 2 ) ) , ( ( W ++ <" Z "> ) ` ( ( N - 2 ) + 1 ) ) } e. E <-> { ( lastS ` W ) , Z } e. E ) )
101 18 100 sylibd 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E -> { ( lastS ` W ) , Z } e. E ) )
102 101 ex 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E -> { ( lastS ` W ) , Z } e. E ) ) )
103 102 com13 
 |-  ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> { ( lastS ` W ) , Z } e. E ) ) )
104 103 3ad2ant2 
 |-  ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> { ( lastS ` W ) , Z } e. E ) ) )
105 104 imp31 
 |-  ( ( ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> { ( lastS ` W ) , Z } e. E )
106 94 adantr 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( W e. Word V /\ Z e. V ) )
107 lswccats1 
 |-  ( ( W e. Word V /\ Z e. V ) -> ( lastS ` ( W ++ <" Z "> ) ) = Z )
108 106 107 syl 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( lastS ` ( W ++ <" Z "> ) ) = Z )
109 63 3ad2ant3 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> 0 < ( N - 1 ) )
110 109 adantr 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> 0 < ( N - 1 ) )
111 65 adantl 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N - 1 ) ) )
112 110 111 mpbird 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> 0 < ( # ` W ) )
113 ccatfv0 
 |-  ( ( W e. Word V /\ <" Z "> e. Word V /\ 0 < ( # ` W ) ) -> ( ( W ++ <" Z "> ) ` 0 ) = ( W ` 0 ) )
114 40 43 112 113 syl3anc 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> ( ( W ++ <" Z "> ) ` 0 ) = ( W ` 0 ) )
115 108 114 preq12d 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( # ` W ) = ( N - 1 ) ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } = { Z , ( W ` 0 ) } )
116 115 ex 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` W ) = ( N - 1 ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } = { Z , ( W ` 0 ) } ) )
117 24 116 syld 
 |-  ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( W ++ <" Z "> ) ) = N -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } = { Z , ( W ` 0 ) } ) )
118 117 impcom 
 |-  ( ( ( # ` ( W ++ <" Z "> ) ) = N /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } = { Z , ( W ` 0 ) } )
119 118 eleq1d 
 |-  ( ( ( # ` ( W ++ <" Z "> ) ) = N /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> ( { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E <-> { Z , ( W ` 0 ) } e. E ) )
120 119 biimpcd 
 |-  ( { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E -> ( ( ( # ` ( W ++ <" Z "> ) ) = N /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> { Z , ( W ` 0 ) } e. E ) )
121 120 3ad2ant3 
 |-  ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) -> ( ( ( # ` ( W ++ <" Z "> ) ) = N /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> { Z , ( W ` 0 ) } e. E ) )
122 121 impl 
 |-  ( ( ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> { Z , ( W ` 0 ) } e. E )
123 105 122 jca 
 |-  ( ( ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) /\ ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) )
124 123 ex 
 |-  ( ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = N ) -> ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) )
125 4 124 biimtrdi 
 |-  ( N e. NN -> ( ( W ++ <" Z "> ) e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) ) )
126 3 125 mpcom 
 |-  ( ( W ++ <" Z "> ) e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) )
127 126 impcom 
 |-  ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" Z "> ) e. ( N ClWWalksN G ) ) -> ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) )