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 bitrid ⊢ 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