Step | Hyp | Ref
| Expression |
1 | | clwwlksext2edg.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wwlknbp 26733 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) |
3 | | simp3 1063 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → 𝑊 ∈ Word 𝑉) |
5 | | s1cl 13382 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑉 → 〈“𝑍”〉 ∈ Word 𝑉) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
〈“𝑍”〉
∈ Word 𝑉) |
7 | | ccatcl 13359 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) |
8 | 4, 6, 7 | syl2an 494 |
. . . . . . 7
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) |
9 | 8 | adantr 481 |
. . . . . 6
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) |
10 | | clwwlksext2edg.e |
. . . . . . . . . . . 12
⊢ 𝐸 = (Edg‘𝐺) |
11 | 1, 10 | wwlknp 26734 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
12 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉) |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉) |
14 | 6 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 〈“𝑍”〉 ∈ Word 𝑉) |
15 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) |
16 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0) |
17 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
18 | 17 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ) |
19 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
20 | 19 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ) |
21 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
22 | 21 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ) |
23 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
25 | 24 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ) |
26 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 < 𝑁) |
27 | 21 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1)) |
28 | 27 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1)) |
29 | 20, 22, 25, 26, 28 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1)) |
30 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1))) |
31 | 16, 18, 29, 30 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1))) |
32 | 15, 31 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1))) |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑊) =
(𝑁 + 1) →
(0..^(#‘𝑊)) =
(0..^(𝑁 +
1))) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (0..^(#‘𝑊)) = (0..^(𝑁 + 1))) |
36 | 35 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
39 | 33, 38 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(#‘𝑊))) |
40 | | ccatval1 13361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = (𝑊‘𝑖)) |
41 | 13, 14, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = (𝑊‘𝑖)) |
42 | 41 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘𝑖)) |
43 | | fzonn0p1p1 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
45 | 34 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑊) =
(𝑁 + 1) → ((𝑖 + 1) ∈ (0..^(#‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))) |
46 | 45 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(#‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))) |
47 | 44, 46 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(#‘𝑊))) |
48 | | ccatval1 13361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
49 | 13, 14, 47, 48 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
50 | 49 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))) |
51 | 42, 50 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))}) |
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
53 | 52 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
54 | 53 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
55 | 54 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
56 | 55 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
57 | 56 | 3impia 1261 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
60 | 59 | impcom 446 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) |
61 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
63 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
64 | 63 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈
ℂ) |
65 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁) |
67 | 62, 66 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 = ((#‘𝑊) − 1)) |
68 | 67 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘𝑁) = ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1))) |
69 | 6 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
〈“𝑍”〉
∈ Word 𝑉) |
70 | | nn0p1gt0 11322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) |
71 | 70 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(𝑁 + 1)) |
72 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑊) =
(𝑁 + 1) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
73 | 72 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
74 | 71, 73 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(#‘𝑊)) |
75 | | hashneq0 13155 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
76 | 12, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(#‘𝑊) ↔ 𝑊 ≠ ∅)) |
77 | 74, 76 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅) |
78 | | ccatval1lsw 13368 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
79 | 12, 69, 77, 78 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
80 | 68, 79 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ( lastS
‘𝑊) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) |
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) = (#‘𝑊) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
82 | 81 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑊) =
(𝑁 + 1) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
83 | 82 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
84 | | ccatws1ls 13410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊)) = 𝑍) |
85 | 84 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊)) = 𝑍) |
86 | 83, 85 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) |
87 | 80, 86 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) |
88 | 87 | 3adantl3 1219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) |
89 | 88 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
90 | 89 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 → {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
91 | 90 | impr 649 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸) |
92 | | simprlr 803 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → 𝑁 ∈
ℕ0) |
93 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑁 → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) |
94 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑁 → (𝑖 + 1) = (𝑁 + 1)) |
95 | 94 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑁 → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) |
96 | 93, 95 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑁 → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) |
97 | 96 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑁 → ({((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
98 | 97 | ralsng 4218 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (∀𝑖 ∈
{𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
99 | 92, 98 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
100 | 91, 99 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) |
101 | | ralunb 3794 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
102 | 60, 100, 101 | sylanbrc 698 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) |
103 | | elnn0uz 11725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
104 | 103 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0)) |
105 | 104 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈
(ℤ≥‘0)) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → 𝑁 ∈
(ℤ≥‘0)) |
107 | | fzosplitsn 12576 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
109 | 108 | raleqdv 3144 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
110 | 102, 109 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) |
111 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → 𝑊 ∈ Word 𝑉) |
112 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸) → 𝑍 ∈ 𝑉) |
113 | | ccatws1len 13398 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (#‘(𝑊 ++ 〈“𝑍”〉)) = ((#‘𝑊) + 1)) |
114 | 111, 112,
113 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (#‘(𝑊 ++ 〈“𝑍”〉)) = ((#‘𝑊) + 1)) |
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ((#‘(𝑊 ++ 〈“𝑍”〉)) − 1) =
(((#‘𝑊) + 1) −
1)) |
116 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) + 1) = ((𝑁 + 1) + 1)) |
117 | 116 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑊) =
(𝑁 + 1) →
(((#‘𝑊) + 1) −
1) = (((𝑁 + 1) + 1) −
1)) |
118 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℂ |
119 | | addcl 10018 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 + 1)
∈ ℂ) |
120 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → 1 ∈ ℂ) |
121 | 119, 120 | pncand 10393 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (((𝑁 + 1) +
1) − 1) = (𝑁 +
1)) |
122 | 63, 118, 121 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
123 | 117, 122 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑊) = (𝑁 + 1)) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)) |
124 | 123 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑊) =
(𝑁 + 1) →
(((#‘𝑊) + 1) −
1) = (𝑁 +
1))) |
125 | 124 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸) → ((#‘𝑊) = (𝑁 + 1) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))) |
126 | 125 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) =
(𝑁 + 1) → (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))) |
127 | 126 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))) |
128 | 127 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)) |
129 | 115, 128 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ((#‘(𝑊 ++ 〈“𝑍”〉)) − 1) = (𝑁 + 1)) |
130 | 129 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)) = (0..^(𝑁 + 1))) |
131 | 130 | raleqdv 3144 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → (∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
132 | 110, 131 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ {( lastS
‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) |
133 | 132 | exp32 631 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
134 | 11, 133 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
135 | 134 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
136 | 135 | imp 445 |
. . . . . . . 8
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
137 | 136 | adantrd 484 |
. . . . . . 7
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
138 | 137 | imp 445 |
. . . . . 6
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) |
139 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word 𝑉) |
140 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝑍 ∈ 𝑉) |
141 | | lswccats1 13411 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ( lastS ‘(𝑊 ++ 〈“𝑍”〉)) = 𝑍) |
142 | 139, 140,
141 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ( lastS
‘(𝑊 ++
〈“𝑍”〉)) = 𝑍) |
143 | 142 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ( lastS ‘(𝑊 ++ 〈“𝑍”〉))) |
144 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉) |
145 | 6 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
〈“𝑍”〉
∈ Word 𝑉) |
146 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 0 <
(𝑁 + 1)) |
147 | 72 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 + 1))) |
148 | 146, 147 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 0 <
(#‘𝑊)) |
149 | 148 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(#‘𝑊)) |
150 | | ccatfv0 13367 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
151 | 150 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊‘0) = ((𝑊 ++ 〈“𝑍”〉)‘0)) |
152 | 144, 145,
149, 151 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑊‘0) = ((𝑊 ++ 〈“𝑍”〉)‘0)) |
153 | 143, 152 | preq12d 4276 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}) |
154 | 153 | exp31 630 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑁 ∈ ℕ0 → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
155 | 154 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈ Word
𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
156 | 155 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}))) |
157 | | wwlknbp2 26752 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) |
158 | 1 | wrdeqi 13328 |
. . . . . . . . . . . . . . . . 17
⊢ Word
𝑉 = Word (Vtx‘𝐺) |
159 | 158 | eqcomi 2631 |
. . . . . . . . . . . . . . . 16
⊢ Word
(Vtx‘𝐺) = Word 𝑉 |
160 | 159 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word (Vtx‘𝐺) ↔ 𝑊 ∈ Word 𝑉) |
161 | 160 | biimpi 206 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉) |
162 | 161 | anim1i 592 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) |
163 | 157, 162 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) |
164 | 156, 163 | impel 485 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)})) |
165 | 164 | imp 445 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)}) |
166 | 165 | eleq1d 2686 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ({𝑍, (𝑊‘0)} ∈ 𝐸 ↔ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) |
167 | 166 | biimpcd 239 |
. . . . . . . 8
⊢ ({𝑍, (𝑊‘0)} ∈ 𝐸 → ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) |
168 | 167 | adantl 482 |
. . . . . . 7
⊢ (({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(
lastS ‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) |
169 | 168 | impcom 446 |
. . . . . 6
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) |
170 | 9, 138, 169 | 3jca 1242 |
. . . . 5
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) |
171 | 113 | ad2ant2r 783 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 ++
〈“𝑍”〉)) = ((#‘𝑊) + 1)) |
172 | 116 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) + 1) = ((𝑁 + 1) + 1)) |
173 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
174 | 63, 173, 173 | addassd 10062 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + (1 +
1))) |
175 | | 1p1e2 11134 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
2 |
176 | 175 | oveq2i 6661 |
. . . . . . . . . . . . . 14
⊢ (𝑁 + (1 + 1)) = (𝑁 + 2) |
177 | 174, 176 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + 2)) |
178 | 177 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) + 1) = (𝑁 + 2)) |
179 | 172, 178 | sylan9eq 2676 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((#‘𝑊) + 1) = (𝑁 + 2)) |
180 | 171, 179 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2)) |
181 | 180 | ex 450 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2))) |
182 | 163, 181 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2))) |
183 | 182 | adantl 482 |
. . . . . . 7
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2))) |
184 | 183 | imp 445 |
. . . . . 6
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2)) |
185 | 184 | adantr 481 |
. . . . 5
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)) |
186 | | 2nn 11185 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
187 | | nn0nnaddcl 11324 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑁 + 2) ∈ ℕ) |
188 | 186, 187 | mpan2 707 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 2) ∈
ℕ) |
189 | 188 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑁 + 2) ∈ ℕ) |
190 | 1, 10 | isclwwlksnx 26889 |
. . . . . . 7
⊢ ((𝑁 + 2) ∈ ℕ →
((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
191 | 189, 190 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
192 | 191 | ad3antrrr 766 |
. . . . 5
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) |
193 | 170, 185,
192 | mpbir2and 957 |
. . . 4
⊢
(((((𝐺 ∈ V
∧ 𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ ({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
194 | 193 | exp31 630 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))) |
195 | 2, 194 | mpancom 703 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))) |
196 | 195 | 3impib 1262 |
1
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |