Step | Hyp | Ref
| Expression |
1 | | wlkcpr 27570 |
. . . . . 6
⊢ (𝑊 ∈ (Walks‘𝐺) ↔ (1st
‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) |
2 | | wlkn0 27562 |
. . . . . 6
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → (2nd ‘𝑊) ≠ ∅) |
3 | 1, 2 | sylbi 220 |
. . . . 5
⊢ (𝑊 ∈ (Walks‘𝐺) → (2nd
‘𝑊) ≠
∅) |
4 | 3 | adantl 485 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → (2nd
‘𝑊) ≠
∅) |
5 | | eqid 2738 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | | eqid 2738 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
7 | | eqid 2738 |
. . . . . . 7
⊢
(1st ‘𝑊) = (1st ‘𝑊) |
8 | | eqid 2738 |
. . . . . . 7
⊢
(2nd ‘𝑊) = (2nd ‘𝑊) |
9 | 5, 6, 7, 8 | wlkelwrd 27574 |
. . . . . 6
⊢ (𝑊 ∈ (Walks‘𝐺) → ((1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺))) |
10 | | ffz0iswrd 13982 |
. . . . . . 7
⊢
((2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺) → (2nd ‘𝑊) ∈ Word (Vtx‘𝐺)) |
11 | 10 | adantl 485 |
. . . . . 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 485 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → (2nd
‘𝑊) ∈ Word
(Vtx‘𝐺)) |
14 | | eqid 2738 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
15 | 14 | upgrwlkvtxedg 27586 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → ∀𝑖 ∈ (0..^(♯‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
16 | | wlklenvm1 27563 |
. . . . . . . . 9
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → (♯‘(1st
‘𝑊)) =
((♯‘(2nd ‘𝑊)) − 1)) |
17 | 16 | adantl 485 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → (♯‘(1st
‘𝑊)) =
((♯‘(2nd ‘𝑊)) − 1)) |
18 | 17 | oveq2d 7186 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) →
(0..^(♯‘(1st ‘𝑊))) = (0..^((♯‘(2nd
‘𝑊)) −
1))) |
19 | 18 | raleqdv 3316 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → (∀𝑖 ∈ (0..^(♯‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
20 | 15, 19 | mpbid 235 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧
(1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) → ∀𝑖 ∈ (0..^((♯‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
21 | 1, 20 | sylan2b 597 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → ∀𝑖 ∈
(0..^((♯‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
22 | 4, 13, 21 | 3jca 1129 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → ((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
23 | 22 | adantr 484 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word (Vtx‘𝐺)
∧ ∀𝑖 ∈
(0..^((♯‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | | simpl 486 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘(1st ‘𝑊)) = 𝑁) → 𝑁 ∈
ℕ0) |
25 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢
((♯‘(1st ‘𝑊)) = 𝑁 → (0...(♯‘(1st
‘𝑊))) = (0...𝑁)) |
26 | 25 | adantl 485 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧
(♯‘(1st ‘𝑊)) = 𝑁) → (0...(♯‘(1st
‘𝑊))) = (0...𝑁)) |
27 | 26 | feq2d 6490 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧
(♯‘(1st ‘𝑊)) = 𝑁) → ((2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺) ↔ (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
28 | 27 | biimpd 232 |
. . . . . . . . . 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 494 |
. . . . . . . 8
⊢
(((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁) → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺))) |
31 | 30 | imp 410 |
. . . . . . 7
⊢
((((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺)) |
32 | | ffz0hash 13897 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (2nd ‘𝑊):(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘(2nd
‘𝑊)) = (𝑁 + 1)) |
33 | 24, 31, 32 | syl2an2 686 |
. . . . . 6
⊢
((((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁)) → (♯‘(2nd
‘𝑊)) = (𝑁 + 1)) |
34 | 33 | ex 416 |
. . . . 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 485 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → ((𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁) → (♯‘(2nd
‘𝑊)) = (𝑁 + 1))) |
37 | 36 | imp 410 |
. 2
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁)) → (♯‘(2nd
‘𝑊)) = (𝑁 + 1)) |
38 | 24 | adantl 485 |
. . 3
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁)) → 𝑁 ∈
ℕ0) |
39 | | iswwlksn 27776 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺) ↔ ((2nd ‘𝑊) ∈ (WWalks‘𝐺) ∧
(♯‘(2nd ‘𝑊)) = (𝑁 + 1)))) |
40 | 5, 14 | iswwlks 27774 |
. . . . . 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 633 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((2nd ‘𝑊) ∈ (WWalks‘𝐺) ∧ (♯‘(2nd
‘𝑊)) = (𝑁 + 1)) ↔ (((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
43 | 39, 42 | bitrd 282 |
. . 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 713 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧
(♯‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺)) |