Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑤 = 𝑡 → ( lastS ‘𝑤) = ( lastS ‘𝑡)) |
2 | | fveq1 6102 |
. . . . 5
⊢ (𝑤 = 𝑡 → (𝑤‘0) = (𝑡‘0)) |
3 | 1, 2 | eqeq12d 2625 |
. . . 4
⊢ (𝑤 = 𝑡 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑡) = (𝑡‘0))) |
4 | | clwwlksbij.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
5 | 3, 4 | elrab2 3333 |
. . 3
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0))) |
6 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
7 | | iswwlksn 41041 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑡 ∈ (𝑁 WWalkSN 𝐺) ↔ (𝑡 ∈ (WWalkS‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalkSN 𝐺) ↔ (𝑡 ∈ (WWalkS‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)))) |
9 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
10 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
11 | 9, 10 | iswwlks 41039 |
. . . . . . . . 9
⊢ (𝑡 ∈ (WWalkS‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (WWalkS‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
13 | 12 | anbi1d 737 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑡 ∈ (WWalkS‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)))) |
14 | 8, 13 | bitrd 267 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalkSN 𝐺) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)))) |
15 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑡 ∈ Word (Vtx‘𝐺)) |
16 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
17 | 6, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
18 | | nnre 10904 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
19 | 18 | lep1d 10834 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1)) |
20 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ0
∧ 𝑁 ≤ (𝑁 + 1))) |
21 | 6, 17, 19, 20 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1))) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(𝑁 + 1))) |
23 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑡) =
(𝑁 + 1) →
(0...(#‘𝑡)) =
(0...(𝑁 +
1))) |
24 | 23 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑡) =
(𝑁 + 1) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
27 | 22, 26 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(#‘𝑡))) |
28 | 15, 27 | jca 553 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)))) |
29 | | swrd0len 13274 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡))) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
31 | 30 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
32 | 31 | 3ad2antl2 1217 |
. . . . . . . . . 10
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
33 | 32 | impcom 445 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
34 | 33 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
35 | | swrdcl 13271 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺)) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺)) |
37 | 36 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺)) |
38 | 37 | ad2antrl 760 |
. . . . . . . . . 10
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺)) |
39 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑡) =
(𝑁 + 1) →
((#‘𝑡) − 1) =
((𝑁 + 1) −
1)) |
40 | 39 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑡) =
(𝑁 + 1) →
(0..^((#‘𝑡) −
1)) = (0..^((𝑁 + 1) −
1))) |
41 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
42 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
43 | 41, 42 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
44 | 43 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 + 1) − 1)) =
(0..^𝑁)) |
45 | 40, 44 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) →
(0..^((#‘𝑡) −
1)) = (0..^𝑁)) |
46 | 45 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
47 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
48 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) |
50 | 18 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ≤ 𝑁) |
51 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁)) |
52 | 49, 47, 50, 51 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘(𝑁 − 1))) |
53 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(0..^(𝑁 − 1)) ⊆
(0..^𝑁)) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
56 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((0..^(𝑁 − 1))
⊆ (0..^𝑁) →
(∀𝑖 ∈
(0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
58 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑡 ∈ Word (Vtx‘𝐺)) |
59 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(𝑁 + 1))) |
60 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
61 | 59, 60 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(#‘𝑡))) |
62 | 61 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(#‘𝑡))) |
63 | 54 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁))) |
64 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁))) |
65 | 64 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
66 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑡 substr 〈0, 𝑁〉)‘𝑖) = (𝑡‘𝑖)) |
67 | 66 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑡‘𝑖) = ((𝑡 substr 〈0, 𝑁〉)‘𝑖)) |
68 | 58, 62, 65, 67 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘𝑖) = ((𝑡 substr 〈0, 𝑁〉)‘𝑖)) |
69 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → 𝑁 ∈ ℤ) |
70 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
71 | 69, 70 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
72 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1)) = (𝑡‘(𝑖 + 1))) |
73 | 72 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))) |
74 | 58, 62, 71, 73 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))) |
75 | 68, 74 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))}) |
76 | 75 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
77 | 76 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
78 | 77 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
79 | 78 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
80 | 79 | com23 84 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
81 | 57, 80 | syld 46 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
82 | 46, 81 | sylbid 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
83 | 82 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ →
((#‘𝑡) = (𝑁 + 1) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
84 | 83 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
85 | 84 | com14 94 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
86 | 85 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
87 | 86 | 3adant1 1072 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
88 | 87 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
89 | 88 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
90 | 89 | ad2antrl 760 |
. . . . . . . . . . 11
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
91 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢
((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 → ((#‘(𝑡 substr 〈0, 𝑁〉)) − 1) = (𝑁 − 1)) |
92 | 91 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 → (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)) =
(0..^(𝑁 −
1))) |
93 | 92 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)) =
(0..^(𝑁 −
1))) |
94 | 93 | raleqdv 3121 |
. . . . . . . . . . 11
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
95 | 90, 94 | mpbird 246 |
. . . . . . . . . 10
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
96 | | simprl2 1100 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑡 ∈ Word (Vtx‘𝐺)) |
97 | 19 | ancli 572 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))) |
98 | 47 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℤ) |
99 | | fznn 12278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) ∈ ℤ →
(𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))) |
101 | 97, 100 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1))) |
102 | 101 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(𝑁 + 1))) |
103 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑡) =
(𝑁 + 1) →
(1...(#‘𝑡)) =
(1...(𝑁 +
1))) |
104 | 103 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑡) =
(𝑁 + 1) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
105 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
106 | 105 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
107 | 102, 106 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(#‘𝑡))) |
108 | 96, 107 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡)))) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡)))) |
110 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))) → ( lastS ‘(𝑡 substr 〈0, 𝑁〉)) = (𝑡‘(𝑁 − 1))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘(𝑡 substr 〈0, 𝑁〉)) = (𝑡‘(𝑁 − 1))) |
112 | | swrd0fv0 13292 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))) → ((𝑡 substr 〈0, 𝑁〉)‘0) = (𝑡‘0)) |
113 | 108, 112 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ((𝑡 substr 〈0, 𝑁〉)‘0) = (𝑡‘0)) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((𝑡 substr 〈0, 𝑁〉)‘0) = (𝑡‘0)) |
115 | 111, 114 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘0)}) |
116 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (( lastS
‘𝑡) = (𝑡‘0) ↔ (𝑡‘0) = ( lastS ‘𝑡)) |
117 | 116 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (( lastS
‘𝑡) = (𝑡‘0) → (𝑡‘0) = ( lastS ‘𝑡)) |
118 | 117 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = ( lastS ‘𝑡)) |
119 | | lsw 13204 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
120 | 119 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
121 | 120 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
123 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → ((#‘𝑡) − 1) = ((𝑁 + 1) − 1)) |
124 | 123, 43 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ((#‘𝑡) − 1) = 𝑁) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((#‘𝑡) − 1) = 𝑁) |
126 | 125 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘((#‘𝑡) − 1)) = (𝑡‘𝑁)) |
127 | 118, 122,
126 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (𝑡‘𝑁)) |
128 | 127 | preq2d 4219 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)}) |
129 | 39, 43 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
((#‘𝑡) − 1) =
𝑁) |
130 | 129 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(0..^((#‘𝑡) −
1)) = (0..^𝑁)) |
131 | 130 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
132 | | fzo0end 12426 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
133 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = (𝑁 − 1) → (𝑡‘𝑖) = (𝑡‘(𝑁 − 1))) |
134 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
135 | 134 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = (𝑁 − 1) → (𝑡‘(𝑖 + 1)) = (𝑡‘((𝑁 − 1) + 1))) |
136 | 133, 135 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = (𝑁 − 1) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))}) |
137 | 136 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = (𝑁 − 1) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))) |
138 | 137 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 − 1) ∈ (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)) |
139 | 132, 138 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)) |
140 | 41, 42 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
141 | 140 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → (𝑡‘((𝑁 − 1) + 1)) = (𝑡‘𝑁)) |
142 | 141 | preq2d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)}) |
143 | 142 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
144 | 143 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
145 | 144 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
146 | 139, 145 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)) |
147 | 146 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
148 | 147 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈
(0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
149 | 131, 148 | sylbid 229 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
150 | 149 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑡) =
(𝑁 + 1) → (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))) |
151 | 150 | com3r 85 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))) |
152 | 151 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))) |
153 | 152 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))) |
154 | 153 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)) |
155 | 154 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)) |
156 | 128, 155 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} ∈ (Edg‘𝐺)) |
157 | 115, 156 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) |
158 | 157 | adantl 481 |
. . . . . . . . . 10
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) |
159 | 38, 95, 158 | 3jca 1235 |
. . . . . . . . 9
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺))) |
160 | | simpl 472 |
. . . . . . . . 9
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
161 | 159, 160 | jca 553 |
. . . . . . . 8
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
162 | 34, 161 | mpancom 700 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
163 | 162 | exp31 628 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (( lastS ‘𝑡) = (𝑡‘0) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)))) |
164 | 14, 163 | sylbid 229 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalkSN 𝐺) → (( lastS ‘𝑡) = (𝑡‘0) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)))) |
165 | 164 | imp32 448 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
166 | 9, 10 | isclwwlksnx 41197 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑡 substr 〈0, 𝑁〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
167 | 166 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ((𝑡 substr 〈0, 𝑁〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ (((𝑡 substr 〈0, 𝑁〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ (Edg‘𝐺)) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
168 | 165, 167 | mpbird 246 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr 〈0, 𝑁〉) ∈ (𝑁 ClWWalkSN 𝐺)) |
169 | 5, 168 | sylan2b 491 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 ∈ 𝐷) → (𝑡 substr 〈0, 𝑁〉) ∈ (𝑁 ClWWalkSN 𝐺)) |
170 | | clwwlksbij.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) |
171 | 169, 170 | fmptd 6292 |
1
⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalkSN 𝐺)) |