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 Word V W W ClWWalks G W ++ ⟨“ W 0 ”⟩ WWalks G

Proof

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