Step | Hyp | Ref
| Expression |
1 | | wlkv 26508 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
2 | | eqid 2622 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2622 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | iswlk 26506 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
5 | | wrdred1 13349 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(𝐹 ↾
(0..^((#‘𝐹) −
1))) ∈ Word dom (iEdg‘𝐺)) |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ∈ Word dom (iEdg‘𝐺) → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
(iEdg‘𝐺))) |
7 | 3 | wlkf 26510 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom (iEdg‘𝐺)) |
8 | | redwlklem 26568 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 1 ≤
(#‘𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶(Vtx‘𝐺)) |
9 | 8 | 3exp 1264 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) → (1
≤ (#‘𝐹) →
(𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶(Vtx‘𝐺)))) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝐹(Walks‘𝐺)𝑃 → (1 ≤ (#‘𝐹) → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶(Vtx‘𝐺)))) |
11 | 10 | imp 445 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶(Vtx‘𝐺))) |
12 | | wlkcl 26511 |
. . . . . . . . 9
⊢ (𝐹(Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
13 | | wrdred1hash 13350 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 1 ≤
(#‘𝐹)) →
(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1)) |
14 | 7, 13 | sylan 488 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) |
15 | | nn0z 11400 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℤ) |
16 | | fzossrbm1 12497 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) ∈
ℤ → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
18 | | ssralv 3666 |
. . . . . . . . . . . . 13
⊢
((0..^((#‘𝐹)
− 1)) ⊆ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) |
20 | 17 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → 𝑘
∈ (0..^(#‘𝐹))) |
21 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0..^(#‘𝐹)) → ((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = (𝑃‘𝑘)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝑃
↾ (0..^(#‘𝐹)))‘𝑘) = (𝑃‘𝑘)) |
23 | 22 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑃‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)) |
24 | | fzo0ss1 12498 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1..^(#‘𝐹))
⊆ (0..^(#‘𝐹)) |
25 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → 𝑘
∈ (0..^((#‘𝐹)
− 1))) |
26 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (#‘𝐹) ∈ ℤ) |
27 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → 1 ∈ ℤ) |
28 | | fzoaddel2 12523 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ (0..^((#‘𝐹) − 1)) ∧
(#‘𝐹) ∈ ℤ
∧ 1 ∈ ℤ) → (𝑘 + 1) ∈ (1..^(#‘𝐹))) |
29 | 25, 26, 27, 28 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑘 + 1)
∈ (1..^(#‘𝐹))) |
30 | 24, 29 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑘 + 1)
∈ (0..^(#‘𝐹))) |
31 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 + 1) ∈ (0..^(#‘𝐹)) → ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝑃
↾ (0..^(#‘𝐹)))‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) |
33 | 32 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))) |
34 | 23, 33 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ↔ ((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)))) |
35 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (0..^((#‘𝐹) − 1)) → ((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘) = (𝐹‘𝑘)) |
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((𝐹
↾ (0..^((#‘𝐹)
− 1)))‘𝑘) =
(𝐹‘𝑘)) |
37 | 36 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (𝐹‘𝑘) = ((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) |
38 | 37 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))) |
39 | 23 | sneqd 4189 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → {(𝑃‘𝑘)} = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}) |
40 | 38, 39 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)} ↔ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)})) |
41 | 23, 33 | preq12d 4276 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))}) |
42 | 41, 38 | sseq12d 3634 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ↔ {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)))) |
43 | 34, 40, 42 | ifpbi123d 1027 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
44 | 43 | biimpd 219 |
. . . . . . . . . . . . 13
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑘
∈ (0..^((#‘𝐹)
− 1))) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
45 | 44 | ralimdva 2962 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
46 | 19, 45 | syld 47 |
. . . . . . . . . . 11
⊢
((#‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
47 | 46 | adantr 481 |
. . . . . . . . . 10
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) →
(∀𝑘 ∈
(0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
48 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1))))) = (0..^((#‘𝐹) − 1))) |
49 | 48 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (0..^((#‘𝐹) − 1)) = (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) −
1)))))) |
50 | 49 | raleqdv 3144 |
. . . . . . . . . . 11
⊢
((#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1) → (∀𝑘 ∈ (0..^((#‘𝐹) − 1))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))) ↔ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
51 | 50 | adantl 482 |
. . . . . . . . . 10
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) →
(∀𝑘 ∈
(0..^((#‘𝐹) −
1))if-(((𝑃 ↾
(0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))) ↔ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
52 | 47, 51 | sylibd 229 |
. . . . . . . . 9
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) →
(∀𝑘 ∈
(0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
53 | 12, 14, 52 | syl2an2r 876 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
54 | 6, 11, 53 | 3anim123d 1406 |
. . . . . . 7
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → ((𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
(iEdg‘𝐺) ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) −
1)))))⟶(Vtx‘𝐺)
∧ ∀𝑘 ∈
(0..^(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))))if-(((𝑃 ↾
(0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)))))) |
55 | 54 | imp 445 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) ∧ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
(iEdg‘𝐺) ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) −
1)))))⟶(Vtx‘𝐺)
∧ ∀𝑘 ∈
(0..^(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))))if-(((𝑃 ↾
(0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘))))) |
56 | | id 22 |
. . . . . . 7
⊢ (𝐺 ∈ V → 𝐺 ∈ V) |
57 | | resexg 5442 |
. . . . . . 7
⊢ (𝐹 ∈ V → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈
V) |
58 | | resexg 5442 |
. . . . . . 7
⊢ (𝑃 ∈ V → (𝑃 ↾ (0..^(#‘𝐹))) ∈ V) |
59 | 2, 3 | iswlk 26506 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧
(𝑃 ↾
(0..^(#‘𝐹))) ∈
V) → ((𝐹 ↾
(0..^((#‘𝐹) −
1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹))) ↔ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
(iEdg‘𝐺) ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) −
1)))))⟶(Vtx‘𝐺)
∧ ∀𝑘 ∈
(0..^(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))))if-(((𝑃 ↾
(0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)))))) |
60 | 59 | bicomd 213 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ V ∧
(𝑃 ↾
(0..^(#‘𝐹))) ∈
V) → (((𝐹 ↾
(0..^((#‘𝐹) −
1))) ∈ Word dom (iEdg‘𝐺) ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))if-(((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)))) ↔ (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹))))) |
61 | 56, 57, 58, 60 | syl3an 1368 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (((𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word dom
(iEdg‘𝐺) ∧ (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) −
1)))))⟶(Vtx‘𝐺)
∧ ∀𝑘 ∈
(0..^(#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))))if-(((𝑃 ↾
(0..^(#‘𝐹)))‘𝑘) = ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1)), ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)) = {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘)}, {((𝑃 ↾ (0..^(#‘𝐹)))‘𝑘), ((𝑃 ↾ (0..^(#‘𝐹)))‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((𝐹 ↾ (0..^((#‘𝐹) − 1)))‘𝑘)))) ↔ (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹))))) |
62 | 55, 61 | syl5ib 234 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) ∧ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹))))) |
63 | 62 | expcomd 454 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹)))))) |
64 | 4, 63 | sylbid 230 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹)))))) |
65 | 1, 64 | mpcom 38 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹))))) |
66 | 65 | anabsi5 858 |
1
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹)))) |