Step | Hyp | Ref
| Expression |
1 | | isclwwlknon 28198 |
. . . . . . 7
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) |
2 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | 2 | clwwlknbp 28142 |
. . . . . . . . 9
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁)) |
4 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑊 ∈ Word
(Vtx‘𝐺)) |
5 | | uzuzle23 12510 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
6 | | eluzfz2 13145 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ (2...𝑁)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ (2...𝑁)) |
8 | 7 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈ (2...𝑁)) |
9 | | oveq2 7240 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑊) =
𝑁 →
(2...(♯‘𝑊)) =
(2...𝑁)) |
10 | 9 | eleq2d 2824 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑊) =
𝑁 → (𝑁 ∈ (2...(♯‘𝑊)) ↔ 𝑁 ∈ (2...𝑁))) |
11 | 10 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 ∈
(2...(♯‘𝑊))
↔ 𝑁 ∈ (2...𝑁))) |
12 | 8, 11 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(2...(♯‘𝑊))) |
13 | 4, 12 | jca 515 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ 𝑁 ∈
(2...(♯‘𝑊)))) |
14 | 13 | ex 416 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ 𝑁 ∈
(2...(♯‘𝑊))))) |
15 | 3, 14 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ 𝑁 ∈
(2...(♯‘𝑊))))) |
16 | 15 | adantr 484 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ 𝑁 ∈
(2...(♯‘𝑊))))) |
17 | 1, 16 | sylbi 220 |
. . . . . 6
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ 𝑁 ∈
(2...(♯‘𝑊))))) |
18 | 17 | impcom 411 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (2...(♯‘𝑊)))) |
19 | | swrds2m 14531 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (2...(♯‘𝑊))) → (𝑊 substr 〈(𝑁 − 2), 𝑁〉) = 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) → (𝑊 substr 〈(𝑁 − 2), 𝑁〉) = 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉) |
21 | 20 | 3adant3 1134 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 substr 〈(𝑁 − 2), 𝑁〉) = 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉) |
22 | | simp3 1140 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊‘(𝑁 − 2)) = (𝑊‘0)) |
23 | | eqidd 2739 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊‘(𝑁 − 1)) = (𝑊‘(𝑁 − 1))) |
24 | 22, 23 | s2eqd 14453 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉 =
〈“(𝑊‘0)(𝑊‘(𝑁 − 1))”〉) |
25 | | simpr 488 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊‘0) = 𝑋) |
26 | | eqidd 2739 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊‘(𝑁 − 1)) = (𝑊‘(𝑁 − 1))) |
27 | 25, 26 | s2eqd 14453 |
. . . . 5
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → 〈“(𝑊‘0)(𝑊‘(𝑁 − 1))”〉 =
〈“𝑋(𝑊‘(𝑁 − 1))”〉) |
28 | 1, 27 | sylbi 220 |
. . . 4
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) → 〈“(𝑊‘0)(𝑊‘(𝑁 − 1))”〉 =
〈“𝑋(𝑊‘(𝑁 − 1))”〉) |
29 | 28 | 3ad2ant2 1136 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → 〈“(𝑊‘0)(𝑊‘(𝑁 − 1))”〉 =
〈“𝑋(𝑊‘(𝑁 − 1))”〉) |
30 | 21, 24, 29 | 3eqtrd 2782 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 substr 〈(𝑁 − 2), 𝑁〉) = 〈“𝑋(𝑊‘(𝑁 − 1))”〉) |
31 | | clwwlknonmpo 28196 |
. . . . 5
⊢
(ClWWalksNOn‘𝐺) = (𝑣 ∈ (Vtx‘𝐺), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
32 | 31 | elmpocl1 7467 |
. . . 4
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) → 𝑋 ∈ (Vtx‘𝐺)) |
33 | 32 | 3ad2ant2 1136 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → 𝑋 ∈ (Vtx‘𝐺)) |
34 | | eluzge3nn 12511 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
35 | | fzo0end 13359 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈ (0..^𝑁)) |
37 | 36 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) ∈
(0..^𝑁)) |
38 | | oveq2 7240 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑊) =
𝑁 →
(0..^(♯‘𝑊)) =
(0..^𝑁)) |
39 | 38 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (0..^(♯‘𝑊)) = (0..^𝑁)) |
40 | 39 | eleq2d 2824 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 1)
∈ (0..^(♯‘𝑊)) ↔ (𝑁 − 1) ∈ (0..^𝑁))) |
41 | 37, 40 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) ∈
(0..^(♯‘𝑊))) |
42 | | wrdsymbcl 14107 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 1) ∈ (0..^(♯‘𝑊))) → (𝑊‘(𝑁 − 1)) ∈ (Vtx‘𝐺)) |
43 | 4, 41, 42 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑊‘(𝑁 − 1)) ∈
(Vtx‘𝐺)) |
44 | 43 | ex 416 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊‘(𝑁 − 1)) ∈
(Vtx‘𝐺))) |
45 | 3, 44 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊‘(𝑁 − 1)) ∈
(Vtx‘𝐺))) |
46 | 45 | adantr 484 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊‘(𝑁 − 1)) ∈
(Vtx‘𝐺))) |
47 | 1, 46 | sylbi 220 |
. . . . 5
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑊‘(𝑁 − 1)) ∈
(Vtx‘𝐺))) |
48 | 47 | impcom 411 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) → (𝑊‘(𝑁 − 1)) ∈ (Vtx‘𝐺)) |
49 | 48 | 3adant3 1134 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊‘(𝑁 − 1)) ∈ (Vtx‘𝐺)) |
50 | | preq1 4664 |
. . . . . . . . 9
⊢ ((𝑊‘0) = 𝑋 → {(𝑊‘0), (𝑊‘(𝑁 − 1))} = {𝑋, (𝑊‘(𝑁 − 1))}) |
51 | 50 | adantl 485 |
. . . . . . . 8
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → {(𝑊‘0), (𝑊‘(𝑁 − 1))} = {𝑋, (𝑊‘(𝑁 − 1))}) |
52 | 51 | eqcomd 2744 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → {𝑋, (𝑊‘(𝑁 − 1))} = {(𝑊‘0), (𝑊‘(𝑁 − 1))}) |
53 | 52 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {𝑋, (𝑊‘(𝑁 − 1))} = {(𝑊‘0), (𝑊‘(𝑁 − 1))}) |
54 | | prcom 4663 |
. . . . . 6
⊢ {(𝑊‘0), (𝑊‘(𝑁 − 1))} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)} |
55 | 53, 54 | eqtrdi 2795 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {𝑋, (𝑊‘(𝑁 − 1))} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
56 | | eqid 2738 |
. . . . . . . . 9
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
57 | 2, 56 | clwwlknp 28144 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
58 | 57 | adantr 484 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
59 | 58 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
60 | | lsw 14144 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
61 | | fvoveq1 7255 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑊) =
𝑁 → (𝑊‘((♯‘𝑊) − 1)) = (𝑊‘(𝑁 − 1))) |
62 | 60, 61 | sylan9eq 2799 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → (lastS‘𝑊) = (𝑊‘(𝑁 − 1))) |
63 | 62 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0))) → (lastS‘𝑊) = (𝑊‘(𝑁 − 1))) |
64 | 63 | preq1d 4670 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0))) → {(lastS‘𝑊), (𝑊‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
65 | 64 | eleq1d 2823 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0))) → ({(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
66 | 65 | biimpd 232 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0))) → ({(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
67 | 66 | ex 416 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → ({(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
68 | 67 | com23 86 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → ({(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
69 | 68 | a1d 25 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ({(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))))) |
70 | 69 | 3imp 1113 |
. . . . . 6
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
71 | 59, 70 | mpcom 38 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)) |
72 | 55, 71 | eqeltrd 2839 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {𝑋, (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺)) |
73 | 1, 72 | syl3an2b 1406 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {𝑋, (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺)) |
74 | | eqid 2738 |
. . . 4
⊢
(ClWWalksNOn‘𝐺) = (ClWWalksNOn‘𝐺) |
75 | 74, 2, 56 | s2elclwwlknon2 28211 |
. . 3
⊢ ((𝑋 ∈ (Vtx‘𝐺) ∧ (𝑊‘(𝑁 − 1)) ∈ (Vtx‘𝐺) ∧ {𝑋, (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺)) → 〈“𝑋(𝑊‘(𝑁 − 1))”〉 ∈ (𝑋(ClWWalksNOn‘𝐺)2)) |
76 | 33, 49, 73, 75 | syl3anc 1373 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → 〈“𝑋(𝑊‘(𝑁 − 1))”〉 ∈ (𝑋(ClWWalksNOn‘𝐺)2)) |
77 | 30, 76 | eqeltrd 2839 |
1
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 substr 〈(𝑁 − 2), 𝑁〉) ∈ (𝑋(ClWWalksNOn‘𝐺)2)) |