Proof of Theorem clwwlknp
Step | Hyp | Ref
| Expression |
1 | | clwwlkbp.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | clwwlknbp0 41192 |
. 2
⊢ (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁))) |
3 | | isclwwlksn 41190 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ↔ (𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 𝑁))) |
4 | 3 | ad2antlr 759 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) → (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ↔ (𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 𝑁))) |
5 | | simpr 476 |
. . . . . 6
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) |
6 | | clwwlknp.e |
. . . . . . . . 9
⊢ 𝐸 = (Edg‘𝐺) |
7 | 1, 6 | isclwwlks 41188 |
. . . . . . . 8
⊢ (𝑊 ∈ (ClWWalkS‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |
8 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) = 𝑁 → ((#‘𝑊) − 1) = (𝑁 − 1)) |
9 | 8 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) = 𝑁 → (0..^((#‘𝑊) − 1)) = (0..^(𝑁 − 1))) |
10 | 9 | raleqdv 3121 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
11 | 10 | biimpd 218 |
. . . . . . . . . . 11
⊢
((#‘𝑊) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
12 | 11 | anim1d 586 |
. . . . . . . . . 10
⊢
((#‘𝑊) = 𝑁 → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
13 | 12 | com12 32 |
. . . . . . . . 9
⊢
((∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = 𝑁 → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
14 | 13 | 3adant1 1072 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((#‘𝑊) = 𝑁 → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
15 | 7, 14 | sylbi 206 |
. . . . . . 7
⊢ (𝑊 ∈ (ClWWalkS‘𝐺) → ((#‘𝑊) = 𝑁 → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
16 | 15 | imp 444 |
. . . . . 6
⊢ ((𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 𝑁) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |
17 | 5, 16 | anim12i 588 |
. . . . 5
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) ∧ (𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 𝑁)) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
18 | | 3anass 1035 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
19 | 17, 18 | sylibr 223 |
. . . 4
⊢ ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) ∧ (𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 𝑁)) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |
20 | 19 | ex 449 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) → ((𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 𝑁) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
21 | 4, 20 | sylbid 229 |
. 2
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) → (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
22 | 2, 21 | mpcom 37 |
1
⊢ (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |