Step | Hyp | Ref
| Expression |
1 | | 1wlkcpr 40833 |
. . . . . 6
⊢ (𝑊 ∈ (1Walks‘𝐺) ↔ (1st
‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) |
2 | | 1wlkn0 40825 |
. . . . . 6
⊢
((1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊) → (2nd ‘𝑊) ≠ ∅) |
3 | 1, 2 | sylbi 206 |
. . . . 5
⊢ (𝑊 ∈ (1Walks‘𝐺) → (2nd
‘𝑊) ≠
∅) |
4 | 3 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) → (2nd
‘𝑊) ≠
∅) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | | eqid 2610 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
7 | | eqid 2610 |
. . . . . . 7
⊢
(1st ‘𝑊) = (1st ‘𝑊) |
8 | | eqid 2610 |
. . . . . . 7
⊢
(2nd ‘𝑊) = (2nd ‘𝑊) |
9 | 5, 6, 7, 8 | 1wlkelwrd 40837 |
. . . . . 6
⊢ (𝑊 ∈ (1Walks‘𝐺) → ((1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺))) |
10 | | ffz0iswrd 13187 |
. . . . . . 7
⊢
((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
11 | 10 | adantl 481 |
. . . . . 6
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ (1Walks‘𝐺) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
13 | 12 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
14 | | eqid 2610 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
15 | 14 | upgr1wlkvtxedg 40853 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) → ∀𝑖 ∈ (0..^(#‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
16 | | 1wlklenvm1 40826 |
. . . . . . . . 9
⊢
((1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊) → (#‘(1st
‘𝑊)) =
((#‘(2nd ‘𝑊)) − 1)) |
17 | 16 | adantl 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) → (#‘(1st
‘𝑊)) =
((#‘(2nd ‘𝑊)) − 1)) |
18 | 17 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) → (0..^(#‘(1st
‘𝑊))) =
(0..^((#‘(2nd ‘𝑊)) − 1))) |
19 | 18 | raleqdv 3121 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) → (∀𝑖 ∈ (0..^(#‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
20 | 15, 19 | mpbid 221 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) → ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
21 | 1, 20 | sylan2b 491 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) → ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
22 | 4, 13, 21 | 3jca 1235 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) → ((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
23 | 22 | adantr 480 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | | simpl 472 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (#‘(1st ‘𝑊)) = 𝑁) → 𝑁 ∈
ℕ0) |
25 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢
((#‘(1st ‘𝑊)) = 𝑁 → (0...(#‘(1st
‘𝑊))) = (0...𝑁)) |
26 | 25 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (#‘(1st
‘𝑊)) = 𝑁) →
(0...(#‘(1st ‘𝑊))) = (0...𝑁)) |
27 | 26 | feq2d 5944 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (#‘(1st
‘𝑊)) = 𝑁) → ((2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) ↔ (2nd
‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
28 | 27 | biimpd 218 |
. . . . . . . . . 10
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (#‘(1st
‘𝑊)) = 𝑁) → ((2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) → (2nd
‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
29 | 28 | impancom 455 |
. . . . . . . . 9
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) →
((#‘(1st ‘𝑊)) = 𝑁 → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
30 | 29 | adantld 482 |
. . . . . . . 8
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
31 | 30 | imp 444 |
. . . . . . 7
⊢
((((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺)) |
32 | | ffz0hash 13088 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺)) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
33 | 24, 31, 32 | syl2an2 871 |
. . . . . 6
⊢
((((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
34 | 33 | ex 449 |
. . . . 5
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (#‘(2nd
‘𝑊)) = (𝑁 + 1))) |
35 | 9, 34 | syl 17 |
. . . 4
⊢ (𝑊 ∈ (1Walks‘𝐺) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (#‘(2nd
‘𝑊)) = (𝑁 + 1))) |
36 | 35 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁) → (#‘(2nd
‘𝑊)) = (𝑁 + 1))) |
37 | 36 | imp 444 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
38 | 24 | adantl 481 |
. . 3
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → 𝑁 ∈
ℕ0) |
39 | | iswwlksn 41041 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((2nd ‘𝑊) ∈ (𝑁 WWalkSN 𝐺) ↔ ((2nd ‘𝑊) ∈ (WWalkS‘𝐺) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
40 | 5, 14 | iswwlks 41039 |
. . . . . 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 737 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((2nd ‘𝑊) ∈ (WWalkS‘𝐺) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)) ↔ (((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
43 | 39, 42 | bitrd 267 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((2nd ‘𝑊) ∈ (𝑁 WWalkSN 𝐺) ↔ (((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
44 | 38, 43 | syl 17 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑊) ∈ (𝑁 WWalkSN 𝐺) ↔ (((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
45 | 23, 37, 44 | mpbir2and 959 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ (𝑁 WWalkSN 𝐺)) |