Step | Hyp | Ref
| Expression |
1 | | wlkcpr 26524 |
. . . . . 6
⊢ (𝑊 ∈ (Walks‘𝐺) ↔ (1st
‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) |
2 | | wlkn0 26516 |
. . . . . 6
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → (2nd ‘𝑊) ≠ ∅) |
3 | 1, 2 | sylbi 207 |
. . . . 5
⊢ (𝑊 ∈ (Walks‘𝐺) → (2nd
‘𝑊) ≠
∅) |
4 | 3 | adantl 482 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → (2nd
‘𝑊) ≠
∅) |
5 | | eqid 2622 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | | eqid 2622 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
7 | | eqid 2622 |
. . . . . . 7
⊢
(1st ‘𝑊) = (1st ‘𝑊) |
8 | | eqid 2622 |
. . . . . . 7
⊢
(2nd ‘𝑊) = (2nd ‘𝑊) |
9 | 5, 6, 7, 8 | wlkelwrd 26528 |
. . . . . 6
⊢ (𝑊 ∈ (Walks‘𝐺) → ((1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺))) |
10 | | ffz0iswrd 13332 |
. . . . . . 7
⊢
((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
11 | 10 | adantl 482 |
. . . . . 6
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ (Walks‘𝐺) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
13 | 12 | adantl 482 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
14 | | eqid 2622 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
15 | 14 | upgrwlkvtxedg 26541 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → ∀𝑖 ∈ (0..^(#‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
16 | | wlklenvm1 26517 |
. . . . . . . . 9
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → (#‘(1st
‘𝑊)) =
((#‘(2nd ‘𝑊)) − 1)) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → (#‘(1st
‘𝑊)) =
((#‘(2nd ‘𝑊)) − 1)) |
18 | 17 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → (0..^(#‘(1st
‘𝑊))) =
(0..^((#‘(2nd ‘𝑊)) − 1))) |
19 | 18 | raleqdv 3144 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → (∀𝑖 ∈ (0..^(#‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
20 | 15, 19 | mpbid 222 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
21 | 1, 20 | sylan2b 492 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
22 | 4, 13, 21 | 3jca 1242 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → ((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
23 | 22 | adantr 481 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | | simpl 473 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (#‘(1st ‘𝑊)) = 𝑁) → 𝑁 ∈
ℕ0) |
25 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢
((#‘(1st ‘𝑊)) = 𝑁 → (0...(#‘(1st
‘𝑊))) = (0...𝑁)) |
26 | 25 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (#‘(1st
‘𝑊)) = 𝑁) →
(0...(#‘(1st ‘𝑊))) = (0...𝑁)) |
27 | 26 | feq2d 6031 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (#‘(1st
‘𝑊)) = 𝑁) → ((2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) ↔ (2nd
‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
28 | 27 | biimpd 219 |
. . . . . . . . . 10
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (#‘(1st
‘𝑊)) = 𝑁) → ((2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) → (2nd
‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
29 | 28 | impancom 456 |
. . . . . . . . 9
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) →
((#‘(1st ‘𝑊)) = 𝑁 → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
30 | 29 | adantld 483 |
. . . . . . . 8
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
31 | 30 | imp 445 |
. . . . . . 7
⊢
((((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺)) |
32 | | ffz0hash 13231 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺)) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
33 | 24, 31, 32 | syl2an2 875 |
. . . . . 6
⊢
((((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
34 | 33 | ex 450 |
. . . . 5
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (#‘(2nd
‘𝑊)) = (𝑁 + 1))) |
35 | 9, 34 | syl 17 |
. . . 4
⊢ (𝑊 ∈ (Walks‘𝐺) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (#‘(2nd
‘𝑊)) = (𝑁 + 1))) |
36 | 35 | adantl 482 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (#‘(2nd
‘𝑊)) = (𝑁 + 1))) |
37 | 36 | imp 445 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
38 | 24 | adantl 482 |
. . 3
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → 𝑁 ∈
ℕ0) |
39 | | iswwlksn 26730 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺) ↔ ((2nd ‘𝑊) ∈ (WWalks‘𝐺) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
40 | 5, 14 | iswwlks 26728 |
. . . . . 6
⊢
((2nd ‘𝑊) ∈ (WWalks‘𝐺) ↔ ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
41 | 40 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((2nd ‘𝑊) ∈ (WWalks‘𝐺) ↔ ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
42 | 41 | anbi1d 741 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((2nd ‘𝑊) ∈ (WWalks‘𝐺) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)) ↔ (((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
43 | 39, 42 | bitrd 268 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺) ↔ (((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
44 | 38, 43 | syl 17 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺) ↔ (((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
45 | 23, 37, 44 | mpbir2and 957 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺)) |