Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))) |
2 | | simplrr 797 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → 𝑊 ∈ Word 𝑉) |
3 | | s1cl 13235 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑉 → 〈“𝑍”〉 ∈ Word 𝑉) |
4 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
〈“𝑍”〉
∈ Word 𝑉) |
5 | | ccatcl 13212 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) |
6 | 2, 4, 5 | syl2an 493 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) |
7 | 6 | adantr 480 |
. . . . . 6
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) |
8 | | wwlknimp 26215 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
9 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉) |
11 | 4 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 〈“𝑍”〉 ∈ Word 𝑉) |
12 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) |
13 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0) |
14 | | peano2nn 10909 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
15 | 14 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ) |
16 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
17 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ) |
18 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
19 | 18 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ) |
20 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
21 | 18, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
22 | 21 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ) |
23 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 < 𝑁) |
24 | 18 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1)) |
25 | 24 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1)) |
26 | 17, 19, 22, 23, 25 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1)) |
27 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1))) |
28 | 13, 15, 26, 27 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1))) |
29 | 12, 28 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1))) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
31 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑊) =
(𝑁 + 1) →
(0..^(#‘𝑊)) =
(0..^(𝑁 +
1))) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (0..^(#‘𝑊)) = (0..^(𝑁 + 1))) |
33 | 32 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
36 | 30, 35 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(#‘𝑊))) |
37 | | ccatval1 13214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = (𝑊‘𝑖)) |
38 | 10, 11, 36, 37 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = (𝑊‘𝑖)) |
39 | 38 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘𝑖)) |
40 | | fzonn0p1p1 12413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
42 | 31 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑊) =
(𝑁 + 1) → ((𝑖 + 1) ∈ (0..^(#‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))) |
43 | 42 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(#‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))) |
44 | 41, 43 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(#‘𝑊))) |
45 | | ccatval1 13214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
46 | 10, 11, 44, 45 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
47 | 46 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))) |
48 | 39, 47 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))}) |
49 | 48 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
50 | 49 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
51 | 50 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
53 | 52 | com23 84 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
54 | 53 | 3impia 1253 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
55 | 54 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
57 | 56 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
58 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
59 | 58 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
60 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
61 | 60 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈
ℂ) |
62 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁) |
64 | 59, 63 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 = ((#‘𝑊) − 1)) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) = ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1))) |
66 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
〈“𝑍”〉
∈ Word 𝑉) |
67 | | nn0p1gt0 11199 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) |
68 | 67 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(𝑁 + 1)) |
69 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑊) =
(𝑁 + 1) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
70 | 69 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
71 | 68, 70 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(#‘𝑊)) |
72 | | hashneq0 13016 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
73 | 9, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(#‘𝑊) ↔ 𝑊 ≠ ∅)) |
74 | 71, 73 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅) |
75 | | ccatval1lsw 13221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
76 | 9, 66, 74, 75 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
77 | 65, 76 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ( lastS
‘𝑊) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) = (#‘𝑊) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
79 | 78 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑊) =
(𝑁 + 1) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
80 | 79 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
81 | | ccatws1ls 13262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊)) = 𝑍) |
82 | 81 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊)) = 𝑍) |
83 | 80, 82 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) |
84 | 77, 83 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) |
85 | 84 | 3adantl3 1212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) |
86 | 85 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
87 | 86 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 → {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
88 | 87 | impr 647 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ ran 𝐸) |
89 | | simprlr 799 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → 𝑁 ∈
ℕ0) |
90 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑁 → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) |
91 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑁 → (𝑖 + 1) = (𝑁 + 1)) |
92 | 91 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑁 → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) |
93 | 90, 92 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑁 → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) |
94 | 93 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑁 → ({((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
95 | 94 | ralsng 4165 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (∀𝑖 ∈
{𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
96 | 89, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ ran 𝐸)) |
97 | 88, 96 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
98 | | ralunb 3756 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
99 | 57, 97, 98 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
100 | | elnn0uz 11601 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
101 | 100 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0)) |
102 | 101 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸) → 𝑁 ∈
(ℤ≥‘0)) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → 𝑁 ∈
(ℤ≥‘0)) |
104 | | fzosplitsn 12442 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
106 | 105 | raleqdv 3121 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
107 | 99, 106 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
108 | | simp1 1054 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → 𝑊 ∈ Word 𝑉) |
109 | | simpll 786 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸) → 𝑍 ∈ 𝑉) |
110 | | ccatws1len 13251 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (#‘(𝑊 ++ 〈“𝑍”〉)) = ((#‘𝑊) + 1)) |
111 | 108, 109,
110 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (#‘(𝑊 ++ 〈“𝑍”〉)) = ((#‘𝑊) + 1)) |
112 | 111 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ((#‘(𝑊 ++ 〈“𝑍”〉)) − 1) =
(((#‘𝑊) + 1) −
1)) |
113 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) + 1) = ((𝑁 + 1) + 1)) |
114 | 113 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑊) =
(𝑁 + 1) →
(((#‘𝑊) + 1) −
1) = (((𝑁 + 1) + 1) −
1)) |
115 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℂ |
116 | | addcl 9897 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 + 1)
∈ ℂ) |
117 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → 1 ∈ ℂ) |
118 | 116, 117 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (((𝑁 + 1) +
1) − 1) = (𝑁 +
1)) |
119 | 60, 115, 118 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
120 | 114, 119 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑊) = (𝑁 + 1)) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)) |
121 | 120 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑊) =
(𝑁 + 1) →
(((#‘𝑊) + 1) −
1) = (𝑁 +
1))) |
122 | 121 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸) → ((#‘𝑊) = (𝑁 + 1) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))) |
123 | 122 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) =
(𝑁 + 1) → (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))) |
124 | 123 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))) |
125 | 124 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)) |
126 | 112, 125 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ((#‘(𝑊 ++ 〈“𝑍”〉)) − 1) = (𝑁 + 1)) |
127 | 126 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)) = (0..^(𝑁 + 1))) |
128 | 127 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → (∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
129 | 107, 128 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
130 | 129 | exp32 629 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
131 | 8, 130 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
132 | 131 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
133 | 132 | imp 444 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
134 | 133 | adantrd 483 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
135 | 134 | imp 444 |
. . . . . 6
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
136 | | wwlknimpb 26232 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) |
137 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word 𝑉) |
138 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝑍 ∈ 𝑉) |
139 | | lswccats1 13263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ( lastS ‘(𝑊 ++ 〈“𝑍”〉)) = 𝑍) |
140 | 137, 138,
139 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ( lastS
‘(𝑊 ++
〈“𝑍”〉)) = 𝑍) |
141 | 140 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ( lastS ‘(𝑊 ++ 〈“𝑍”〉))) |
142 | 137 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉) |
143 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
〈“𝑍”〉
∈ Word 𝑉) |
144 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 0 <
(𝑁 + 1)) |
145 | 69 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
146 | 144, 145 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 0 <
(#‘𝑊)) |
147 | 146 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(#‘𝑊)) |
148 | | ccatfv0 13220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
149 | 148 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊‘0) = ((𝑊 ++ 〈“𝑍”〉)‘0)) |
150 | 142, 143,
147, 149 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑊‘0) = ((𝑊 ++ 〈“𝑍”〉)‘0)) |
151 | 141, 150 | preq12d 4220 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}) |
152 | 151 | exp31 628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑁 ∈ ℕ0 → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
153 | 152 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈ Word
𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
154 | 153 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
156 | 136, 155 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
157 | 156 | impcom 445 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)})) |
158 | 157 | imp 444 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}) |
159 | 158 | eleq1d 2672 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({𝑍, (𝑊‘0)} ∈ ran 𝐸 ↔ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸)) |
160 | 159 | biimpcd 238 |
. . . . . . . 8
⊢ ({𝑍, (𝑊‘0)} ∈ ran 𝐸 → (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸)) |
161 | 160 | adantl 481 |
. . . . . . 7
⊢ (({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸) → (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸)) |
162 | 161 | impcom 445 |
. . . . . 6
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) |
163 | 7, 135, 162 | 3jca 1235 |
. . . . 5
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸)) |
164 | 110 | ad2ant2r 779 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 ++
〈“𝑍”〉)) = ((#‘𝑊) + 1)) |
165 | 113 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) + 1) = ((𝑁 + 1) + 1)) |
166 | 115 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
167 | 60, 166, 166 | addassd 9941 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + (1 +
1))) |
168 | | 1p1e2 11011 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
2 |
169 | 168 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ (𝑁 + (1 + 1)) = (𝑁 + 2) |
170 | 167, 169 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + 2)) |
171 | 170 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) + 1) = (𝑁 + 2)) |
172 | 165, 171 | sylan9eq 2664 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((#‘𝑊) + 1) = (𝑁 + 2)) |
173 | 164, 172 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2)) |
174 | 173 | ex 449 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2))) |
175 | 136, 174 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2))) |
176 | 175 | adantl 481 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2))) |
177 | 176 | imp 444 |
. . . . . 6
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2)) |
178 | 177 | adantr 480 |
. . . . 5
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)) |
179 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
180 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
181 | 180 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℕ0) |
182 | 179, 181 | nn0addcld 11232 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 2) ∈
ℕ0) |
183 | 182 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑁 + 2) ∈
ℕ0) |
184 | 183 | anim2i 591 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 + 2) ∈
ℕ0)) |
185 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 2) ∈
ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 + 2) ∈
ℕ0)) |
186 | 184, 185 | sylibr 223 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 2) ∈
ℕ0)) |
187 | | isclwwlkn 26297 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 2) ∈
ℕ0) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
188 | 186, 187 | syl 17 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
189 | | isclwwlk 26296 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸))) |
190 | 189 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸))) |
191 | 190 | anbi1d 737 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
192 | 188, 191 | bitrd 267 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
193 | 192 | ad3antrrr 762 |
. . . . 5
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
194 | 163, 178,
193 | mpbir2and 959 |
. . . 4
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))) |
195 | 194 | exp31 628 |
. . 3
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))))) |
196 | 1, 195 | mpancom 700 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))))) |
197 | 196 | 3impib 1254 |
1
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)))) |