Step | Hyp | Ref
| Expression |
1 | | wlkbprop 26051 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
2 | | iswlk 26048 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
3 | 2 | 3adant1 1072 |
. . . 4
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
4 | | wrdf 13165 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
5 | | nn0z 11277 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℤ) |
6 | | fzossrbm1 12366 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℤ → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) ∈
ℕ0 → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
8 | | fssres 5983 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) → (𝐹 ↾ (0..^((#‘𝐹) − 1))):(0..^((#‘𝐹) − 1))⟶dom 𝐸) |
9 | 7, 8 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) → (𝐹 ↾ (0..^((#‘𝐹) −
1))):(0..^((#‘𝐹)
− 1))⟶dom 𝐸) |
10 | | iswrdi 13164 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ (0..^((#‘𝐹) −
1))):(0..^((#‘𝐹)
− 1))⟶dom 𝐸
→ (𝐹 ↾
(0..^((#‘𝐹) −
1))) ∈ Word dom 𝐸) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
𝐸) |
12 | 11 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((#‘𝐹) ∈ ℕ0 → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
𝐸)) |
13 | 4, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ0
→ (𝐹 ↾
(0..^((#‘𝐹) −
1))) ∈ Word dom 𝐸)) |
14 | 13 | com12 32 |
. . . . . . . . . 10
⊢
((#‘𝐹) ∈
ℕ0 → (𝐹 ∈ Word dom 𝐸 → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸)) |
15 | 14 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹 ∈ Word dom 𝐸 → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸)) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → (𝐹 ∈ Word dom 𝐸 → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸)) |
17 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
18 | | fzossfz 12357 |
. . . . . . . . . . 11
⊢
(0..^(#‘𝐹))
⊆ (0...(#‘𝐹)) |
19 | | fssres 5983 |
. . . . . . . . . . 11
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))) → (𝑃 ↾ (0..^(#‘𝐹))):(0..^(#‘𝐹))⟶𝑉) |
20 | 17, 18, 19 | sylancl 693 |
. . . . . . . . . 10
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝑃 ↾ (0..^(#‘𝐹))):(0..^(#‘𝐹))⟶𝑉) |
21 | 20 | ex 449 |
. . . . . . . . 9
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝑃 ↾ (0..^(#‘𝐹))):(0..^(#‘𝐹))⟶𝑉)) |
22 | | redwlklem 26135 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) |
23 | | fzoval 12340 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) ∈
ℤ → (0..^(#‘𝐹)) = (0...((#‘𝐹) − 1))) |
24 | 5, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ0 → (0..^(#‘𝐹)) = (0...((#‘𝐹) − 1))) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ (#‘𝐹) ∈ ℕ0)
→ (0..^(#‘𝐹)) =
(0...((#‘𝐹) −
1))) |
26 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ (#‘𝐹) ∈ ℕ0)
→ (#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1)) |
27 | 26 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ (#‘𝐹) ∈ ℕ0)
→ (0...(#‘(𝐹
↾ (0..^((#‘𝐹)
− 1))))) = (0...((#‘𝐹) − 1))) |
28 | 25, 27 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ (#‘𝐹) ∈ ℕ0)
→ (0..^(#‘𝐹)) =
(0...(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))))) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . 14
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → ((#‘𝐹) ∈ ℕ0 →
(0..^(#‘𝐹)) =
(0...(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1))))))) |
30 | 22, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → ((#‘𝐹) ∈ ℕ0 →
(0..^(#‘𝐹)) =
(0...(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1))))))) |
31 | 30 | com12 32 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (0..^(#‘𝐹)) = (0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1))))))) |
32 | 31 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (0..^(#‘𝐹)) = (0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1))))))) |
33 | 32 | imp 444 |
. . . . . . . . . 10
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → (0..^(#‘𝐹)) = (0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))) |
34 | 33 | feq2d 5944 |
. . . . . . . . 9
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → ((𝑃 ↾ (0..^(#‘𝐹))):(0..^(#‘𝐹))⟶𝑉 ↔ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉)) |
35 | 21, 34 | sylibd 228 |
. . . . . . . 8
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉)) |
36 | 7 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (0..^((#‘𝐹) − 1)) ⊆
(0..^(#‘𝐹))) |
37 | | ssralv 3629 |
. . . . . . . . . . . . . . 15
⊢
((0..^((#‘𝐹)
− 1)) ⊆ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
39 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (0..^((#‘𝐹) − 1)) → ((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘) = (𝐹‘𝑘)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝐹
↾ (0..^((#‘𝐹)
− 1)))‘𝑘) =
(𝐹‘𝑘)) |
41 | 40 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝐹‘𝑘) = ((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) |
42 | 41 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝐸‘(𝐹‘𝑘)) = (𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))) |
43 | 7 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → 𝑘
∈ (0..^(#‘𝐹))) |
44 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (0..^(#‘𝐹)) → ((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = (𝑃‘𝑘)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝑃
↾ (0..^(#‘𝐹)))‘𝑘) = (𝑃‘𝑘)) |
46 | 45 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑃‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)) |
47 | | fzo0ss1 12367 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1..^(#‘𝐹))
⊆ (0..^(#‘𝐹)) |
48 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → 𝑘
∈ (0..^((#‘𝐹)
− 1))) |
49 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (#‘𝐹) ∈ ℤ) |
50 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → 1 ∈ ℤ) |
51 | | fzoaddel2 12391 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ (0..^((#‘𝐹) − 1)) ∧
(#‘𝐹) ∈ ℤ
∧ 1 ∈ ℤ) → (𝑘 + 1) ∈ (1..^(#‘𝐹))) |
52 | 48, 49, 50, 51 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑘 + 1)
∈ (1..^(#‘𝐹))) |
53 | 47, 52 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑘 + 1)
∈ (0..^(#‘𝐹))) |
54 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 + 1) ∈ (0..^(#‘𝐹)) → ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝑃
↾ (0..^(#‘𝐹)))‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) |
56 | 55 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))) |
57 | 46, 56 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}) |
58 | 42, 57 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
59 | 58 | biimpd 218 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
60 | 59 | 3ad2antl1 1216 |
. . . . . . . . . . . . . . 15
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑘 ∈ (0..^((#‘𝐹) − 1))) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
61 | 60 | ralimdva 2945 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
62 | 38, 61 | syld 46 |
. . . . . . . . . . . . 13
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
63 | 62 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ ((#‘𝐹) ∈ ℕ0
∧ (𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) →
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
64 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1))))) = (0..^((#‘𝐹) − 1))) |
65 | 64 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (0..^((#‘𝐹) − 1)) = (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) −
1)))))) |
66 | 65 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (∀𝑘 ∈ (0..^((#‘𝐹) − 1))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
67 | 66 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ ((#‘𝐹) ∈ ℕ0
∧ (𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) →
(∀𝑘 ∈
(0..^((#‘𝐹) −
1))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
68 | 63, 67 | sylibd 228 |
. . . . . . . . . . 11
⊢
(((#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = ((#‘𝐹) − 1) ∧ ((#‘𝐹) ∈ ℕ0
∧ (𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) →
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
69 | 68 | ex 449 |
. . . . . . . . . 10
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}))) |
70 | 22, 69 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}))) |
71 | 70 | impcom 445 |
. . . . . . . 8
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))})) |
72 | 16, 35, 71 | 3anim123d 1398 |
. . . . . . 7
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹))) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸 ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}))) |
73 | 72 | expimpd 627 |
. . . . . 6
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸 ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}))) |
74 | | resexg 5362 |
. . . . . . . . . 10
⊢ (𝐹 ∈ V → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈
V) |
75 | | resexg 5362 |
. . . . . . . . . 10
⊢ (𝑃 ∈ V → (𝑃 ↾ (0..^(#‘𝐹))) ∈ V) |
76 | 74, 75 | anim12i 588 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧
(𝑃 ↾
(0..^(#‘𝐹))) ∈
V)) |
77 | 76 | anim2i 591 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧
(𝑃 ↾
(0..^(#‘𝐹))) ∈
V))) |
78 | 77 | 3adant1 1072 |
. . . . . . 7
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧ (𝑃 ↾ (0..^(#‘𝐹))) ∈ V))) |
79 | | iswlk 26048 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧
(𝑃 ↾
(0..^(#‘𝐹))) ∈
V)) → ((𝐹 ↾
(0..^((#‘𝐹) −
1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹))) ↔ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸 ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}))) |
80 | 79 | bicomd 212 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧
(𝑃 ↾
(0..^(#‘𝐹))) ∈
V)) → (((𝐹 ↾
(0..^((#‘𝐹) −
1))) ∈ Word dom 𝐸
∧ (𝑃 ↾
(0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}) ↔ (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹))))) |
81 | 78, 80 | syl 17 |
. . . . . 6
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom 𝐸 ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))(𝐸‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}) ↔ (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹))))) |
82 | 73, 81 | sylibd 228 |
. . . . 5
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹))))) |
83 | 82 | expcomd 453 |
. . . 4
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹)))))) |
84 | 3, 83 | sylbid 229 |
. . 3
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹)))))) |
85 | 1, 84 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹))))) |
86 | 85 | anabsi5 854 |
1
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹)))) |