Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2610 |
. . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | iswwlks 41039 |
. . 3
⊢ (𝑊 ∈ (WWalkS‘𝐺) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
4 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (#‘𝑊) ∈
ℕ0) |
5 | | simpl 472 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈
ℕ0) |
6 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 1 ∈ ℝ) |
7 | | 2re 10967 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 2 ∈ ℝ) |
9 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℝ) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈ ℝ) |
11 | | 1le2 11118 |
. . . . . . . . . . . . . . 15
⊢ 1 ≤
2 |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 1 ≤ 2) |
13 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 2 ≤ (#‘𝑊)) |
14 | 6, 8, 10, 12, 13 | letrd 10073 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊)) |
15 | 5, 14 | jca 553 |
. . . . . . . . . . . 12
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) ∈ ℕ0 ∧ 1 ≤
(#‘𝑊))) |
16 | | elnnnn0c 11215 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ ↔ ((#‘𝑊)
∈ ℕ0 ∧ 1 ≤ (#‘𝑊))) |
17 | 15, 16 | sylibr 223 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
18 | | lbfzo0 12375 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^(#‘𝑊)) ↔
(#‘𝑊) ∈
ℕ) |
19 | 17, 18 | sylibr 223 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 0 ∈ (0..^(#‘𝑊))) |
20 | | nn0ge2m1nn 11237 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
ℕ) |
21 | | lbfzo0 12375 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^((#‘𝑊) −
1)) ↔ ((#‘𝑊)
− 1) ∈ ℕ) |
22 | 20, 21 | sylibr 223 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 0 ∈ (0..^((#‘𝑊) − 1))) |
23 | 19, 22 | jca 553 |
. . . . . . . . 9
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (0 ∈ (0..^(#‘𝑊)) ∧ 0 ∈
(0..^((#‘𝑊) −
1)))) |
24 | 4, 23 | sylan 487 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (0 ∈
(0..^(#‘𝑊)) ∧ 0
∈ (0..^((#‘𝑊)
− 1)))) |
25 | | inelcm 3984 |
. . . . . . . 8
⊢ ((0
∈ (0..^(#‘𝑊))
∧ 0 ∈ (0..^((#‘𝑊) − 1))) → ((0..^(#‘𝑊)) ∩ (0..^((#‘𝑊) − 1))) ≠
∅) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((0..^(#‘𝑊)) ∩ (0..^((#‘𝑊) − 1))) ≠
∅) |
27 | | wrdfn 13174 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 Fn (0..^(#‘𝑊))) |
28 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → 𝑊 Fn (0..^(#‘𝑊))) |
29 | | fnresdisj 5915 |
. . . . . . . . . 10
⊢ (𝑊 Fn (0..^(#‘𝑊)) → (((0..^(#‘𝑊)) ∩ (0..^((#‘𝑊) − 1))) = ∅ ↔
(𝑊 ↾
(0..^((#‘𝑊) −
1))) = ∅)) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (((0..^(#‘𝑊)) ∩ (0..^((#‘𝑊) − 1))) = ∅ ↔
(𝑊 ↾
(0..^((#‘𝑊) −
1))) = ∅)) |
31 | | nn0ge2m1nn0 11238 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
ℕ0) |
32 | 10 | lem1d 10836 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ≤ (#‘𝑊)) |
33 | 31, 5, 32 | 3jca 1235 |
. . . . . . . . . . . 12
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (((#‘𝑊) − 1) ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ ((#‘𝑊) − 1) ≤ (#‘𝑊))) |
34 | 4, 33 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (((#‘𝑊) − 1) ∈
ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧
((#‘𝑊) − 1)
≤ (#‘𝑊))) |
35 | | elfz2nn0 12300 |
. . . . . . . . . . 11
⊢
(((#‘𝑊)
− 1) ∈ (0...(#‘𝑊)) ↔ (((#‘𝑊) − 1) ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ ((#‘𝑊) − 1) ≤ (#‘𝑊))) |
36 | 34, 35 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) |
37 | | swrd0val 13273 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) →
(𝑊 substr 〈0,
((#‘𝑊) −
1)〉) = (𝑊 ↾
(0..^((#‘𝑊) −
1)))) |
38 | 37 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) →
((𝑊 substr 〈0,
((#‘𝑊) −
1)〉) = ∅ ↔ (𝑊 ↾ (0..^((#‘𝑊) − 1))) = ∅)) |
39 | 38 | bicomd 212 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) →
((𝑊 ↾
(0..^((#‘𝑊) −
1))) = ∅ ↔ (𝑊
substr 〈0, ((#‘𝑊) − 1)〉) =
∅)) |
40 | 36, 39 | syldan 486 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((𝑊 ↾ (0..^((#‘𝑊) − 1))) = ∅ ↔ (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) =
∅)) |
41 | 30, 40 | bitr2d 268 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) = ∅ ↔
((0..^(#‘𝑊)) ∩
(0..^((#‘𝑊) −
1))) = ∅)) |
42 | 41 | necon3bid 2826 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ≠ ∅ ↔
((0..^(#‘𝑊)) ∩
(0..^((#‘𝑊) −
1))) ≠ ∅)) |
43 | 26, 42 | mpbird 246 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ≠
∅) |
44 | 43 | 3ad2antl2 1217 |
. . . . 5
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺)) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ≠
∅) |
45 | | swrdcl 13271 |
. . . . . . . 8
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ Word
(Vtx‘𝐺)) |
46 | 45 | a1d 25 |
. . . . . . 7
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (2 ≤ (#‘𝑊) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ Word
(Vtx‘𝐺))) |
47 | 46 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺)) → (2 ≤ (#‘𝑊) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ Word
(Vtx‘𝐺))) |
48 | 47 | imp 444 |
. . . . 5
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺)) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ Word
(Vtx‘𝐺)) |
49 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℤ) |
50 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) ∈
ℤ → ((#‘𝑊)
− 1) ∈ ℤ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) − 1) ∈
ℤ) |
52 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑊)
− 1) ∈ ℤ → (((#‘𝑊) − 1) − 1) ∈
ℤ) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) ∈
ℕ0 → (((#‘𝑊) − 1) − 1) ∈
ℤ) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (((#‘𝑊) − 1) − 1) ∈
ℤ) |
55 | 51 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
ℤ) |
56 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) ∈
ℝ → ((#‘𝑊)
− 1) ∈ ℝ) |
57 | 9, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) − 1) ∈
ℝ) |
58 | 57 | lem1d 10836 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) ∈
ℕ0 → (((#‘𝑊) − 1) − 1) ≤ ((#‘𝑊) − 1)) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (((#‘𝑊) − 1) − 1) ≤ ((#‘𝑊) − 1)) |
60 | 54, 55, 59 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((((#‘𝑊) − 1) − 1) ∈ ℤ ∧
((#‘𝑊) − 1)
∈ ℤ ∧ (((#‘𝑊) − 1) − 1) ≤ ((#‘𝑊) − 1))) |
61 | 4, 60 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((((#‘𝑊) − 1) − 1) ∈
ℤ ∧ ((#‘𝑊)
− 1) ∈ ℤ ∧ (((#‘𝑊) − 1) − 1) ≤ ((#‘𝑊) − 1))) |
62 | | eluz2 11569 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊)
− 1) ∈ (ℤ≥‘(((#‘𝑊) − 1) − 1)) ↔
((((#‘𝑊) − 1)
− 1) ∈ ℤ ∧ ((#‘𝑊) − 1) ∈ ℤ ∧
(((#‘𝑊) − 1)
− 1) ≤ ((#‘𝑊) − 1))) |
63 | 61, 62 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
(ℤ≥‘(((#‘𝑊) − 1) − 1))) |
64 | 9 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) − 1) ≤ (#‘𝑊)) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ≤ (#‘𝑊)) |
66 | 31, 5, 65 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → (((#‘𝑊) − 1) ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ ((#‘𝑊) − 1) ≤ (#‘𝑊))) |
67 | 4, 66 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (((#‘𝑊) − 1) ∈
ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧
((#‘𝑊) − 1)
≤ (#‘𝑊))) |
68 | 67, 35 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) |
69 | | swrd0len 13274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) →
(#‘(𝑊 substr 〈0,
((#‘𝑊) −
1)〉)) = ((#‘𝑊)
− 1)) |
70 | 69 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊))) →
((#‘(𝑊 substr
〈0, ((#‘𝑊)
− 1)〉)) − 1) = (((#‘𝑊) − 1) − 1)) |
71 | 68, 70 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)
= (((#‘𝑊) − 1)
− 1)) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) →
(ℤ≥‘((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)) =
(ℤ≥‘(((#‘𝑊) − 1) − 1))) |
73 | 63, 72 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
(ℤ≥‘((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) −
1))) |
74 | | fzoss2 12365 |
. . . . . . . . . . . 12
⊢
(((#‘𝑊)
− 1) ∈ (ℤ≥‘((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)) →
(0..^((#‘(𝑊 substr
〈0, ((#‘𝑊)
− 1)〉)) − 1)) ⊆ (0..^((#‘𝑊) − 1))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1))
⊆ (0..^((#‘𝑊)
− 1))) |
76 | | ssralv 3629 |
. . . . . . . . . . 11
⊢
((0..^((#‘(𝑊
substr 〈0, ((#‘𝑊) − 1)〉)) − 1)) ⊆
(0..^((#‘𝑊) −
1)) → (∀𝑥
∈ (0..^((#‘𝑊)
− 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
78 | 68, 69 | syldan 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) =
((#‘𝑊) −
1)) |
79 | 78 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)
= (((#‘𝑊) − 1)
− 1)) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1))
= (0..^(((#‘𝑊)
− 1) − 1))) |
81 | 80 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)) ↔
𝑥 ∈
(0..^(((#‘𝑊) −
1) − 1)))) |
82 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → 𝑊 ∈ Word (Vtx‘𝐺)) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → 𝑊 ∈ Word (Vtx‘𝐺)) |
84 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) →
((#‘𝑊) − 1)
∈ (0...(#‘𝑊))) |
85 | 4, 31 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
ℕ0) |
86 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑊)
− 1) ∈ ℕ0 → ((#‘𝑊) − 1) ∈
ℤ) |
87 | | fzossrbm1 12366 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑊)
− 1) ∈ ℤ → (0..^(((#‘𝑊) − 1) − 1)) ⊆
(0..^((#‘𝑊) −
1))) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑊)
− 1) ∈ ℕ0 → (0..^(((#‘𝑊) − 1) − 1)) ⊆
(0..^((#‘𝑊) −
1))) |
89 | 85, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (0..^(((#‘𝑊) − 1) − 1)) ⊆
(0..^((#‘𝑊) −
1))) |
90 | 89 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → 𝑥 ∈ (0..^((#‘𝑊) − 1))) |
91 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊)) ∧
𝑥 ∈
(0..^((#‘𝑊) −
1))) → ((𝑊 substr
〈0, ((#‘𝑊)
− 1)〉)‘𝑥)
= (𝑊‘𝑥)) |
92 | 83, 84, 90, 91 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥) = (𝑊‘𝑥)) |
93 | 92 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → (𝑊‘𝑥) = ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥)) |
94 | 4, 20 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) − 1) ∈
ℕ) |
95 | | elfzom1p1elfzo 12414 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((#‘𝑊)
− 1) ∈ ℕ ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → (𝑥 + 1) ∈
(0..^((#‘𝑊) −
1))) |
96 | 94, 95 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → (𝑥 + 1) ∈
(0..^((#‘𝑊) −
1))) |
97 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊)) ∧
(𝑥 + 1) ∈
(0..^((#‘𝑊) −
1))) → ((𝑊 substr
〈0, ((#‘𝑊)
− 1)〉)‘(𝑥
+ 1)) = (𝑊‘(𝑥 + 1))) |
98 | 83, 84, 96, 97 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1)) = (𝑊‘(𝑥 + 1))) |
99 | 98 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → (𝑊‘(𝑥 + 1)) = ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))) |
100 | 93, 99 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1))) → {(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} = {((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))}) |
101 | 100 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (𝑥 ∈ (0..^(((#‘𝑊) − 1) − 1)) → {(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} = {((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))})) |
102 | 81, 101 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)) →
{(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} = {((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))})) |
103 | 102 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1))) →
{(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} = {((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))}) |
104 | 103 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1))) →
({(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
105 | 104 | biimpd 218 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) ∧ 𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1))) →
({(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → {((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
106 | 105 | ralimdva 2945 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) −
1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
107 | 77, 106 | syld 46 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
108 | 107 | expcom 450 |
. . . . . . . 8
⊢ (2 ≤
(#‘𝑊) → (𝑊 ∈ Word (Vtx‘𝐺) → (∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺)))) |
109 | 108 | com3l 87 |
. . . . . . 7
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → (2 ≤ (#‘𝑊) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺)))) |
110 | 109 | a1i 11 |
. . . . . 6
⊢ (𝑊 ≠ ∅ → (𝑊 ∈ Word (Vtx‘𝐺) → (∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺) → (2 ≤ (#‘𝑊) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺))))) |
111 | 110 | 3imp1 1272 |
. . . . 5
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺)) ∧ 2 ≤ (#‘𝑊)) → ∀𝑥 ∈ (0..^((#‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺)) |
112 | 1, 2 | iswwlks 41039 |
. . . . 5
⊢ ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈
(WWalkS‘𝐺) ↔
((𝑊 substr 〈0,
((#‘𝑊) −
1)〉) ≠ ∅ ∧ (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑥 ∈
(0..^((#‘(𝑊 substr
〈0, ((#‘𝑊)
− 1)〉)) − 1)){((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝑥), ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘(𝑥 + 1))} ∈ (Edg‘𝐺))) |
113 | 44, 48, 111, 112 | syl3anbrc 1239 |
. . . 4
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺)) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈
(WWalkS‘𝐺)) |
114 | 113 | ex 449 |
. . 3
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑥), (𝑊‘(𝑥 + 1))} ∈ (Edg‘𝐺)) → (2 ≤ (#‘𝑊) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈
(WWalkS‘𝐺))) |
115 | 3, 114 | sylbi 206 |
. 2
⊢ (𝑊 ∈ (WWalkS‘𝐺) → (2 ≤ (#‘𝑊) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈
(WWalkS‘𝐺))) |
116 | 115 | imp 444 |
1
⊢ ((𝑊 ∈ (WWalkS‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈
(WWalkS‘𝐺)) |