Proof of Theorem wwlknimp
Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))) |
2 | | iswwlkn 26212 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1)))) |
3 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1))) → (#‘𝑊) = (𝑁 + 1)) |
4 | | iswwlk 26211 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ (𝑉 WWalks 𝐸) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
5 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
6 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
7 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
8 | 6, 7 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) − 1) = 𝑁) |
10 | 5, 9 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) − 1) = 𝑁) |
11 | 10 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑊) = (𝑁 + 1)) →
(0..^((#‘𝑊) −
1)) = (0..^𝑁)) |
12 | 11 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑊) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
13 | 12 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑊) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
14 | 13 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘𝑊) = (𝑁 + 1) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
15 | 14 | com23 84 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑊) = (𝑁 + 1) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
16 | 15 | impancom 455 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑁 ∈ ℕ0 →
((#‘𝑊) = (𝑁 + 1) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
17 | 16 | 3adant1 1072 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑁 ∈ ℕ0 →
((#‘𝑊) = (𝑁 + 1) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
18 | 4, 17 | syl6bi 242 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ (𝑉 WWalks 𝐸) → (𝑁 ∈ ℕ0 →
((#‘𝑊) = (𝑁 + 1) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)))) |
19 | 18 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ ℕ0
→ (𝑊 ∈ (𝑉 WWalks 𝐸) → ((#‘𝑊) = (𝑁 + 1) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)))) |
20 | 19 | 3impia 1253 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ (𝑉 WWalks 𝐸) → ((#‘𝑊) = (𝑁 + 1) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
21 | 20 | imp32 448 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) |
22 | 3, 21 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1))) → ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
23 | 22 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
24 | 2, 23 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
25 | 24 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
26 | 25 | ancoms 468 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑉 ∈ V ∧
𝐸 ∈ V)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
27 | 26 | imp 444 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ (𝑉 ∈ V ∧
𝐸 ∈ V)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
28 | 27 | anim2i 591 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((𝑁 ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
29 | | 3anass 1035 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
30 | 28, 29 | sylibr 223 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((𝑁 ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
31 | 30 | exp44 639 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))))) |
32 | 31 | impcom 445 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)))) |
33 | 32 | impcom 445 |
. 2
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) |
34 | 1, 33 | mpcom 37 |
1
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |