Metamath Proof Explorer

Theorem clwwlkel

Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Hypothesis clwwlkf1o.d 
|- D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
Assertion clwwlkel 
|- ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. D )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d 
 |-  D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
2 ccatws1n0 
 |-  ( P e. Word ( Vtx ` G ) -> ( P ++ <" ( P ` 0 ) "> ) =/= (/) )
3 2 adantr 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( P ++ <" ( P ` 0 ) "> ) =/= (/) )
4 3 3ad2ant2 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( P ++ <" ( P ` 0 ) "> ) =/= (/) )
5 simprl 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> P e. Word ( Vtx ` G ) )
6 fstwrdne0 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( P ` 0 ) e. ( Vtx ` G ) )
7 6 s1cld 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> <" ( P ` 0 ) "> e. Word ( Vtx ` G ) )
8 ccatcl 
 |-  ( ( P e. Word ( Vtx ` G ) /\ <" ( P ` 0 ) "> e. Word ( Vtx ` G ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) )
9 5 7 8 syl2anc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) )
10 9 3adant3 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) )
11 5 adantr 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> P e. Word ( Vtx ` G ) )
12 7 adantr 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> <" ( P ` 0 ) "> e. Word ( Vtx ` G ) )
13 elfzonn0 
 |-  ( i e. ( 0 ..^ ( N - 1 ) ) -> i e. NN0 )
14 13 adantl 
 |-  ( ( N e. NN /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i e. NN0 )
15 nnz 
 |-  ( N e. NN -> N e. ZZ )
16 15 adantr 
 |-  ( ( N e. NN /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> N e. ZZ )
17 elfzo0 
 |-  ( i e. ( 0 ..^ ( N - 1 ) ) <-> ( i e. NN0 /\ ( N - 1 ) e. NN /\ i < ( N - 1 ) ) )
18 nn0re 
 |-  ( i e. NN0 -> i e. RR )
19 18 adantr 
 |-  ( ( i e. NN0 /\ N e. NN ) -> i e. RR )
20 nnre 
 |-  ( N e. NN -> N e. RR )
21 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
22 20 21 syl 
 |-  ( N e. NN -> ( N - 1 ) e. RR )
23 22 adantl 
 |-  ( ( i e. NN0 /\ N e. NN ) -> ( N - 1 ) e. RR )
24 20 adantl 
 |-  ( ( i e. NN0 /\ N e. NN ) -> N e. RR )
25 19 23 24 3jca 
 |-  ( ( i e. NN0 /\ N e. NN ) -> ( i e. RR /\ ( N - 1 ) e. RR /\ N e. RR ) )
26 25 adantr 
 |-  ( ( ( i e. NN0 /\ N e. NN ) /\ i < ( N - 1 ) ) -> ( i e. RR /\ ( N - 1 ) e. RR /\ N e. RR ) )
27 20 ltm1d 
 |-  ( N e. NN -> ( N - 1 ) < N )
28 27 adantl 
 |-  ( ( i e. NN0 /\ N e. NN ) -> ( N - 1 ) < N )
29 28 anim1ci 
 |-  ( ( ( i e. NN0 /\ N e. NN ) /\ i < ( N - 1 ) ) -> ( i < ( N - 1 ) /\ ( N - 1 ) < N ) )
30 lttr 
 |-  ( ( i e. RR /\ ( N - 1 ) e. RR /\ N e. RR ) -> ( ( i < ( N - 1 ) /\ ( N - 1 ) < N ) -> i < N ) )
31 26 29 30 sylc 
 |-  ( ( ( i e. NN0 /\ N e. NN ) /\ i < ( N - 1 ) ) -> i < N )
32 31 ex 
 |-  ( ( i e. NN0 /\ N e. NN ) -> ( i < ( N - 1 ) -> i < N ) )
33 32 impancom 
 |-  ( ( i e. NN0 /\ i < ( N - 1 ) ) -> ( N e. NN -> i < N ) )
34 33 3adant2 
 |-  ( ( i e. NN0 /\ ( N - 1 ) e. NN /\ i < ( N - 1 ) ) -> ( N e. NN -> i < N ) )
35 17 34 sylbi 
 |-  ( i e. ( 0 ..^ ( N - 1 ) ) -> ( N e. NN -> i < N ) )
36 35 impcom 
 |-  ( ( N e. NN /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i < N )
37 elfzo0z 
 |-  ( i e. ( 0 ..^ N ) <-> ( i e. NN0 /\ N e. ZZ /\ i < N ) )
38 14 16 36 37 syl3anbrc 
 |-  ( ( N e. NN /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i e. ( 0 ..^ N ) )
39 38 adantlr 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i e. ( 0 ..^ N ) )
40 oveq2 
 |-  ( ( # ` P ) = N -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ N ) )
41 40 eleq2d 
 |-  ( ( # ` P ) = N -> ( i e. ( 0 ..^ ( # ` P ) ) <-> i e. ( 0 ..^ N ) ) )
42 41 ad2antll 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( i e. ( 0 ..^ ( # ` P ) ) <-> i e. ( 0 ..^ N ) ) )
43 42 adantr 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i e. ( 0 ..^ ( # ` P ) ) <-> i e. ( 0 ..^ N ) ) )
44 39 43 mpbird 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> i e. ( 0 ..^ ( # ` P ) ) )
45 ccatval1 
 |-  ( ( P e. Word ( Vtx ` G ) /\ <" ( P ` 0 ) "> e. Word ( Vtx ` G ) /\ i e. ( 0 ..^ ( # ` P ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` i ) = ( P ` i ) )
46 11 12 44 45 syl3anc 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` i ) = ( P ` i ) )
47 elfzom1p1elfzo 
 |-  ( ( N e. NN /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ N ) )
48 47 adantlr 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ N ) )
49 40 ad2antll 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ N ) )
50 49 adantr 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ N ) )
51 48 50 eleqtrrd 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` P ) ) )
52 ccatval1 
 |-  ( ( P e. Word ( Vtx ` G ) /\ <" ( P ` 0 ) "> e. Word ( Vtx ` G ) /\ ( i + 1 ) e. ( 0 ..^ ( # ` P ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
53 11 12 51 52 syl3anc 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
54 46 53 preq12d 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
55 54 eleq1d 
 |-  ( ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) /\ i e. ( 0 ..^ ( N - 1 ) ) ) -> ( { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
56 55 ralbidva 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
57 56 biimprcd 
 |-  ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
58 57 adantr 
 |-  ( ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) -> ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
59 58 expdcom 
 |-  ( N e. NN -> ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
60 59 3imp 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
61 fzo0end 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) )
62 40 eleq2d 
 |-  ( ( # ` P ) = N -> ( ( N - 1 ) e. ( 0 ..^ ( # ` P ) ) <-> ( N - 1 ) e. ( 0 ..^ N ) ) )
63 62 adantl 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( ( N - 1 ) e. ( 0 ..^ ( # ` P ) ) <-> ( N - 1 ) e. ( 0 ..^ N ) ) )
64 61 63 syl5ibrcom 
 |-  ( N e. NN -> ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( N - 1 ) e. ( 0 ..^ ( # ` P ) ) ) )
65 64 imp 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( N - 1 ) e. ( 0 ..^ ( # ` P ) ) )
66 ccatval1 
 |-  ( ( P e. Word ( Vtx ` G ) /\ <" ( P ` 0 ) "> e. Word ( Vtx ` G ) /\ ( N - 1 ) e. ( 0 ..^ ( # ` P ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) = ( P ` ( N - 1 ) ) )
67 5 7 65 66 syl3anc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) = ( P ` ( N - 1 ) ) )
68 lsw 
 |-  ( P e. Word ( Vtx ` G ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
69 68 adantr 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
70 fvoveq1 
 |-  ( ( # ` P ) = N -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( N - 1 ) ) )
71 70 adantl 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( N - 1 ) ) )
72 69 71 eqtr2d 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( P ` ( N - 1 ) ) = ( lastS ` P ) )
73 72 adantl 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( P ` ( N - 1 ) ) = ( lastS ` P ) )
74 67 73 eqtr2d 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( lastS ` P ) = ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) )
75 nncn 
 |-  ( N e. NN -> N e. CC )
76 1cnd 
 |-  ( N e. NN -> 1 e. CC )
77 75 76 npcand 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
78 77 fveq2d 
 |-  ( N e. NN -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` N ) )
79 78 adantr 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` N ) )
80 fveq2 
 |-  ( ( # ` P ) = N -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( # ` P ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` N ) )
81 80 ad2antll 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( # ` P ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` N ) )
82 ccatws1ls 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( P ` 0 ) e. ( Vtx ` G ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( # ` P ) ) = ( P ` 0 ) )
83 5 6 82 syl2anc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( # ` P ) ) = ( P ` 0 ) )
84 79 81 83 3eqtr2rd 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( P ` 0 ) = ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) )
85 74 84 preq12d 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> { ( lastS ` P ) , ( P ` 0 ) } = { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } )
86 85 eleq1d 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) <-> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
87 86 biimpcd 
 |-  ( { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) -> ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
88 87 adantl 
 |-  ( ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) -> ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
89 88 expdcom 
 |-  ( N e. NN -> ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) -> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
90 89 3imp 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) )
91 ovex 
 |-  ( N - 1 ) e. _V
92 fveq2 
 |-  ( i = ( N - 1 ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` i ) = ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) )
93 fvoveq1 
 |-  ( i = ( N - 1 ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) )
94 92 93 preq12d 
 |-  ( i = ( N - 1 ) -> { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } = { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } )
95 94 eleq1d 
 |-  ( i = ( N - 1 ) -> ( { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
96 91 95 ralsn 
 |-  ( A. i e. { ( N - 1 ) } { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( P ++ <" ( P ` 0 ) "> ) ` ( N - 1 ) ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( ( N - 1 ) + 1 ) ) } e. ( Edg ` G ) )
97 90 96 sylibr 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> A. i e. { ( N - 1 ) } { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
98 75 76 76 addsubd 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
99 98 oveq2d 
 |-  ( N e. NN -> ( 0 ..^ ( ( N + 1 ) - 1 ) ) = ( 0 ..^ ( ( N - 1 ) + 1 ) ) )
100 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
101 elnn0uz 
 |-  ( ( N - 1 ) e. NN0 <-> ( N - 1 ) e. ( ZZ>= ` 0 ) )
102 100 101 sylib 
 |-  ( N e. NN -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
103 fzosplitsn 
 |-  ( ( N - 1 ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( N - 1 ) + 1 ) ) = ( ( 0 ..^ ( N - 1 ) ) u. { ( N - 1 ) } ) )
104 102 103 syl 
 |-  ( N e. NN -> ( 0 ..^ ( ( N - 1 ) + 1 ) ) = ( ( 0 ..^ ( N - 1 ) ) u. { ( N - 1 ) } ) )
105 99 104 eqtrd 
 |-  ( N e. NN -> ( 0 ..^ ( ( N + 1 ) - 1 ) ) = ( ( 0 ..^ ( N - 1 ) ) u. { ( N - 1 ) } ) )
106 105 raleqdv 
 |-  ( N e. NN -> ( A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( N - 1 ) ) u. { ( N - 1 ) } ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
107 ralunb 
 |-  ( A. i e. ( ( 0 ..^ ( N - 1 ) ) u. { ( N - 1 ) } ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( N - 1 ) } { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
108 106 107 bitrdi 
 |-  ( N e. NN -> ( A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( N - 1 ) } { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
109 108 3ad2ant1 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( N - 1 ) } { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
110 60 97 109 mpbir2and 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
111 ccatlen 
 |-  ( ( P e. Word ( Vtx ` G ) /\ <" ( P ` 0 ) "> e. Word ( Vtx ` G ) ) -> ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) )
112 5 7 111 syl2anc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) )
113 id 
 |-  ( ( # ` P ) = N -> ( # ` P ) = N )
114 s1len 
 |-  ( # ` <" ( P ` 0 ) "> ) = 1
115 114 a1i 
 |-  ( ( # ` P ) = N -> ( # ` <" ( P ` 0 ) "> ) = 1 )
116 113 115 oveq12d 
 |-  ( ( # ` P ) = N -> ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) = ( N + 1 ) )
117 116 ad2antll 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( ( # ` P ) + ( # ` <" ( P ` 0 ) "> ) ) = ( N + 1 ) )
118 112 117 eqtrd 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) )
119 118 3adant3 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) )
120 119 oveq1d 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) = ( ( N + 1 ) - 1 ) )
121 120 oveq2d 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) = ( 0 ..^ ( ( N + 1 ) - 1 ) ) )
122 121 raleqdv 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( N + 1 ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
123 110 122 mpbird 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
124 4 10 123 3jca 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) =/= (/) /\ ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
125 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
126 iswwlksn 
 |-  ( N e. NN0 -> ( ( P ++ <" ( P ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( P ++ <" ( P ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) ) ) )
127 125 126 syl 
 |-  ( N e. NN -> ( ( P ++ <" ( P ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( P ++ <" ( P ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) ) ) )
128 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
129 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
130 128 129 iswwlks 
 |-  ( ( P ++ <" ( P ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( P ++ <" ( P ` 0 ) "> ) =/= (/) /\ ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
131 130 anbi1i 
 |-  ( ( ( P ++ <" ( P ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) ) <-> ( ( ( P ++ <" ( P ` 0 ) "> ) =/= (/) /\ ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) ) )
132 127 131 bitrdi 
 |-  ( N e. NN -> ( ( P ++ <" ( P ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( ( P ++ <" ( P ` 0 ) "> ) =/= (/) /\ ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) ) ) )
133 132 3ad2ant1 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( ( P ++ <" ( P ` 0 ) "> ) =/= (/) /\ ( P ++ <" ( P ` 0 ) "> ) e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` ( P ++ <" ( P ` 0 ) "> ) ) - 1 ) ) { ( ( P ++ <" ( P ` 0 ) "> ) ` i ) , ( ( P ++ <" ( P ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` ( P ++ <" ( P ` 0 ) "> ) ) = ( N + 1 ) ) ) )
134 124 119 133 mpbir2and 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. ( N WWalksN G ) )
135 lswccats1 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( P ` 0 ) e. ( Vtx ` G ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( P ` 0 ) )
136 5 6 135 syl2anc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( P ` 0 ) )
137 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
138 137 biimpri 
 |-  ( N e. NN -> 0 e. ( 0 ..^ N ) )
139 40 eleq2d 
 |-  ( ( # ` P ) = N -> ( 0 e. ( 0 ..^ ( # ` P ) ) <-> 0 e. ( 0 ..^ N ) ) )
140 139 adantl 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> ( 0 e. ( 0 ..^ ( # ` P ) ) <-> 0 e. ( 0 ..^ N ) ) )
141 138 140 syl5ibrcom 
 |-  ( N e. NN -> ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) -> 0 e. ( 0 ..^ ( # ` P ) ) ) )
142 141 imp 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> 0 e. ( 0 ..^ ( # ` P ) ) )
143 ccatval1 
 |-  ( ( P e. Word ( Vtx ` G ) /\ <" ( P ` 0 ) "> e. Word ( Vtx ` G ) /\ 0 e. ( 0 ..^ ( # ` P ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) = ( P ` 0 ) )
144 5 7 142 143 syl3anc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) = ( P ` 0 ) )
145 136 144 eqtr4d 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )
146 145 3adant3 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )
147 fveq2 
 |-  ( w = ( P ++ <" ( P ` 0 ) "> ) -> ( lastS ` w ) = ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) )
148 fveq1 
 |-  ( w = ( P ++ <" ( P ` 0 ) "> ) -> ( w ` 0 ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )
149 147 148 eqeq12d 
 |-  ( w = ( P ++ <" ( P ` 0 ) "> ) -> ( ( lastS ` w ) = ( w ` 0 ) <-> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) ) )
150 149 1 elrab2 
 |-  ( ( P ++ <" ( P ` 0 ) "> ) e. D <-> ( ( P ++ <" ( P ` 0 ) "> ) e. ( N WWalksN G ) /\ ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) ) )
151 134 146 150 sylanbrc 
 |-  ( ( N e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` P ) , ( P ` 0 ) } e. ( Edg ` G ) ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. D )