Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))) |
2 | | simpl 472 |
. . . . . . 7
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑁 + 1) ∈
ℕ0) |
3 | 2 | anim2i 591 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 + 1) ∈
ℕ0)) |
4 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 1) ∈
ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 + 1) ∈
ℕ0)) |
5 | 3, 4 | sylibr 223 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 1) ∈
ℕ0)) |
6 | | iswwlkn 26212 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 1) ∈
ℕ0) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)))) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)))) |
8 | | iswwlk 26211 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ (𝑉 WWalks 𝐸) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ (𝑉 WWalks 𝐸) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
10 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word 𝑉) |
11 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
12 | 11 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℕ) |
13 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
14 | 13 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
15 | 14 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
16 | 15 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
17 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(#‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) ≤ (#‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
19 | 16, 18 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ (#‘𝑊)) |
20 | | swrdn0 13282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ ℕ ∧ (𝑁 + 1) ≤ (#‘𝑊)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅) |
21 | 10, 12, 19, 20 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅) |
22 | 21 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Word 𝑉 → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅))) |
23 | 22 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅))) |
24 | 23 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅)) |
25 | 24 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅)) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅)) |
27 | 26 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅) |
28 | | swrdcl 13271 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉) |
29 | 28 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉) |
32 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((#‘𝑊) − 1) =
(((𝑁 + 1) + 1) −
1)) |
33 | 13 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
34 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
35 | 33, 34 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
36 | 32, 35 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((#‘𝑊) −
1) = (𝑁 +
1)) |
37 | 36 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (0..^((#‘𝑊)
− 1)) = (0..^(𝑁 +
1))) |
38 | 37 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
40 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
41 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
42 | 13, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
43 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
44 | 43 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ (𝑁 + 1)) |
45 | 40, 42, 44 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℤ
∧ (𝑁 + 1) ∈
ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
46 | 45 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
47 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
48 | 46, 47 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
49 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
51 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((0..^𝑁) ⊆
(0..^(𝑁 + 1)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
53 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉) |
55 | | nn0fz0 12306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑁 + 1) ∈ ℕ0
↔ (𝑁 + 1) ∈
(0...(𝑁 +
1))) |
56 | 13, 55 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...(𝑁 +
1))) |
57 | 56 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...(𝑁 + 1))) |
58 | | fzelp1 12263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑁 + 1) ∈ (0...(𝑁 + 1)) → (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1))) |
60 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
(0...(#‘𝑊)) =
(0...((𝑁 + 1) +
1))) |
61 | 60 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ∈
(0...(#‘𝑊)) ↔
(𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)))) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 + 1) ∈
(0...(#‘𝑊)) ↔
(𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)))) |
63 | 62 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) ∈ (0...(#‘𝑊)) ↔ (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)))) |
64 | 59, 63 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...(#‘𝑊))) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑁 + 1) ∈ (0...(#‘𝑊))) |
66 | | fzossfzop1 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
67 | 66 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℕ0
→ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
68 | 67 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
69 | 68 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
70 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)) ∧ 𝑖 ∈ (0..^(𝑁 + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖) = (𝑊‘𝑖)) |
71 | 54, 65, 69, 70 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖) = (𝑊‘𝑖)) |
72 | 71 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘𝑖) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖)) |
73 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁)) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁)) |
75 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
76 | 75 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑁 ∈ ℤ →
(0..^(𝑁 + 1)) = (0...𝑁)) |
77 | 40, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
(0...𝑁)) |
78 | 77 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ0
→ ((𝑖 + 1) ∈
(0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
79 | 78 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
81 | 74, 80 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
82 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^(𝑁 + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
83 | 54, 65, 81, 82 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
84 | 83 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘(𝑖 + 1)) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))) |
85 | 72, 84 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))}) |
86 | 85 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
87 | 86 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → {((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
88 | 87 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
89 | 52, 88 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
90 | 39, 89 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
91 | 90 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
92 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
93 | 92, 34 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ (0..^((𝑁 + 1)
− 1)) = (0..^𝑁)) |
95 | 94 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((𝑁 + 1) − 1)) =
(0..^𝑁)) |
96 | 95 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (0..^((𝑁 + 1) − 1)) = (0..^𝑁)) |
97 | 96 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
98 | 91, 97 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
99 | 13 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
ℕ0) |
100 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (#‘𝑊) =
((𝑁 + 1) +
1)) |
101 | 100 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(#‘𝑊) = ((𝑁 + 1) + 1)) |
102 | | swrd0len0 13288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ ℕ0 ∧
(#‘𝑊) = ((𝑁 + 1) + 1)) →
(#‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑁 + 1)) |
103 | 53, 99, 101, 102 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑁 + 1)) |
104 | 103 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1) = ((𝑁 + 1)
− 1)) |
105 | 104 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)) = (0..^((𝑁 + 1)
− 1))) |
106 | 105 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
108 | 98, 107 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
109 | 108 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ Word 𝑉 → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
110 | 109 | com23 84 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ Word 𝑉 → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
111 | 110 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
112 | 111 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
113 | 112 | expd 451 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
114 | 113 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
115 | 114 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
117 | 116 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
118 | 27, 31, 117 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅ ∧ (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
119 | | iswwlk 26211 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅ ∧ (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 substr 〈0,
(𝑁 + 1)〉) ∈
(𝑉 WWalks 𝐸) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅ ∧ (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
121 | 120 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅ ∧ (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
122 | 118, 121 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸)) |
123 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
124 | 13, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
125 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)) ↔ ((𝑁 + 1) ∈ ℕ0
∧ ((𝑁 + 1) + 1) ∈
ℕ0 ∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
126 | 13, 124, 15, 125 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
127 | 126 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
128 | 127, 62 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...(#‘𝑊))) |
129 | 128 | anim2i 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))) |
130 | 129 | exp32 629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ Word 𝑉 → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))))) |
131 | 130 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))))) |
132 | 131 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
133 | 132 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
134 | 133 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
135 | 134 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))) |
136 | | swrd0len 13274 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)) |
138 | | iswwlkn 26212 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 substr 〈0,
(𝑁 + 1)〉) ∈
((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
139 | 138 | 3expa 1257 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 substr 〈0,
(𝑁 + 1)〉) ∈
((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
140 | 139 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
141 | 122, 137,
140 | mpbir2and 959 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
142 | 141 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (((𝑊 ≠ ∅
∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
143 | 142 | expcom 450 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑉 ∈ V ∧
𝐸 ∈ V) → (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
144 | 143 | com3l 87 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
145 | 144 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
146 | 145 | expd 451 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))))) |
147 | 9, 146 | sylbid 229 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ (𝑉 WWalks 𝐸) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))))) |
148 | 147 | impd 446 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
149 | 7, 148 | sylbid 229 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
150 | 1, 149 | mpcom 37 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
151 | 150 | com12 32 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |