| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | | eqid 2737 |
. . 3
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 3 | 1, 2 | wwlknp 29863 |
. 2
⊢ (𝑊 ∈ (𝑀 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 4 | | pfxcl 14715 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺)) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺)) |
| 6 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺)) |
| 7 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑊 ∈ Word (Vtx‘𝐺)) |
| 8 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ ℕ) |
| 9 | | eluz2 12884 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀)) |
| 10 | | zre 12617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 11 | | zre 12617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
| 12 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ≤ 𝑀 → 𝑁 ≤ 𝑀) |
| 13 | 10, 11, 12 | 3anim123i 1152 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ≤ 𝑀)) |
| 14 | 9, 13 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ≤ 𝑀)) |
| 15 | | letrp1 12111 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ≤ 𝑀) → 𝑁 ≤ (𝑀 + 1)) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ (𝑀 + 1)) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ (𝑀 + 1)) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ≤ (𝑀 + 1)) |
| 19 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑊) =
(𝑀 + 1) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1))) |
| 20 | 19 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1))) |
| 21 | 18, 20 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ≤ (♯‘𝑊)) |
| 22 | | pfxn0 14724 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝑊)) → (𝑊 prefix 𝑁) ≠ ∅) |
| 23 | 7, 8, 21, 22 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑊 prefix 𝑁) ≠ ∅) |
| 24 | 6, 23 | jca 511 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅)) |
| 25 | 24 | 3adantl3 1169 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅)) |
| 26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅)) |
| 27 | | nnz 12634 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 28 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ0 |
| 29 | | eluzmn 12885 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 1 ∈
ℕ0) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
| 30 | 27, 28, 29 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘(𝑁 − 1))) |
| 31 | | uzss 12901 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘(𝑁 − 1))) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘(𝑁 − 1))) |
| 33 | 32 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘(𝑁 − 1))) |
| 34 | | fzoss2 13727 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀)) |
| 36 | 35 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀)) |
| 37 | | ssralv 4052 |
. . . . . . . . . . . . 13
⊢
((0..^(𝑁 − 1))
⊆ (0..^𝑀) →
(∀𝑖 ∈
(0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 39 | 38 | 3exp 1120 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
| 40 | 39 | com34 91 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
| 41 | 40 | 3imp1 1348 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 42 | 41 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 43 | | nnnn0 12533 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 44 | | elnn0uz 12923 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
| 45 | 43, 44 | sylib 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘0)) |
| 46 | | eluzfz 13559 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (0...𝑀)) |
| 47 | 45, 46 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ (0...𝑀)) |
| 48 | | fzelp1 13616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (0...𝑀) → 𝑁 ∈ (0...(𝑀 + 1))) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ (0...(𝑀 + 1))) |
| 50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (0...(𝑀 + 1))) |
| 51 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑊) =
(𝑀 + 1) →
(0...(♯‘𝑊)) =
(0...(𝑀 +
1))) |
| 52 | 51 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑊) =
(𝑀 + 1) → (𝑁 ∈
(0...(♯‘𝑊))
↔ 𝑁 ∈ (0...(𝑀 + 1)))) |
| 53 | 52 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1)))) |
| 54 | 50, 53 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (0...(♯‘𝑊))) |
| 55 | | pfxlen 14721 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝑁)) = 𝑁) |
| 56 | 7, 54, 55 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (♯‘(𝑊 prefix 𝑁)) = 𝑁) |
| 57 | 56 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) →
((♯‘(𝑊 prefix
𝑁)) − 1) = (𝑁 − 1)) |
| 58 | 57 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) →
(0..^((♯‘(𝑊
prefix 𝑁)) − 1)) =
(0..^(𝑁 −
1))) |
| 59 | 58 | raleqdv 3326 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 60 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑊 ∈ Word (Vtx‘𝐺)) |
| 61 | 54 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑊))) |
| 62 | 30 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
| 63 | | fzoss2 13727 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
| 65 | 64 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
| 66 | | pfxfv 14720 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 prefix 𝑁)‘𝑖) = (𝑊‘𝑖)) |
| 67 | 60, 61, 65, 66 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 prefix 𝑁)‘𝑖) = (𝑊‘𝑖)) |
| 68 | 27 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ ℤ) |
| 69 | | elfzom1elp1fzo 13771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
| 70 | 68, 69 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
| 71 | | pfxfv 14720 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑊 prefix 𝑁)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
| 72 | 60, 61, 70, 71 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 prefix 𝑁)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
| 73 | 67, 72 | preq12d 4741 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}) |
| 74 | 73 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 75 | 74 | ralbidva 3176 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 76 | 59, 75 | bitrd 279 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 77 | 76 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 78 | 77 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 79 | 42, 78 | mpbird 257 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 80 | | elfz1uz 13634 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ (1...𝑀)) |
| 81 | | fzelp1 13616 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (1...𝑀) → 𝑁 ∈ (1...(𝑀 + 1))) |
| 82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ (1...(𝑀 + 1))) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (1...(𝑀 + 1))) |
| 84 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑊) =
(𝑀 + 1) →
(1...(♯‘𝑊)) =
(1...(𝑀 +
1))) |
| 85 | 84 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑊) =
(𝑀 + 1) → (𝑁 ∈
(1...(♯‘𝑊))
↔ 𝑁 ∈ (1...(𝑀 + 1)))) |
| 86 | 85 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1)))) |
| 87 | 83, 86 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (1...(♯‘𝑊))) |
| 88 | | pfxfvlsw 14733 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 prefix 𝑁)) = (𝑊‘(𝑁 − 1))) |
| 89 | | pfxfv0 14730 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝑁)‘0) = (𝑊‘0)) |
| 90 | 88, 89 | preq12d 4741 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
| 91 | 7, 87, 90 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
| 92 | 91 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
| 93 | 92 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
| 94 | | fz1fzo0m1 13750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (1...𝑀) → (𝑁 − 1) ∈ (0..^𝑀)) |
| 95 | 80, 94 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → (𝑁 − 1) ∈ (0..^𝑀)) |
| 96 | 95 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑁 − 1) ∈ (0..^𝑀)) |
| 97 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → 𝑖 = (𝑁 − 1)) |
| 98 | 97 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘𝑖) = (𝑊‘(𝑁 − 1))) |
| 99 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
| 100 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 101 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
| 103 | 99, 102 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑖 + 1) = 𝑁) |
| 104 | 103 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊‘𝑁)) |
| 105 | 98, 104 | preq12d 4741 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
| 106 | 105 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))) |
| 107 | 106 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑖 = (𝑁 − 1) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)))) |
| 108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → (𝑖 = (𝑁 − 1) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)))) |
| 109 | 108 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑖 = (𝑁 − 1) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)))) |
| 110 | 109 | imp 406 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))) |
| 111 | 96, 110 | rspcdv 3614 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))) |
| 112 | 111 | 3exp 1120 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))))) |
| 113 | 112 | com34 91 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))))) |
| 114 | 113 | 3imp1 1348 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)) |
| 115 | 114 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)) |
| 116 | | preq2 4734 |
. . . . . . . . . . 11
⊢ ((𝑊‘𝑁) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)}) |
| 117 | 116 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝑊‘𝑁) = (𝑊‘0) → ({(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
| 118 | 117 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → ({(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
| 119 | 115, 118 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)) |
| 120 | 93, 119 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) |
| 121 | 26, 79, 120 | 3jca 1129 |
. . . . . 6
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))) |
| 122 | 121 | exp31 419 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → ((𝑊‘𝑁) = (𝑊‘0) → (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))))) |
| 123 | 122 | 3imp21 1114 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))) |
| 124 | 1, 2 | isclwwlk 30003 |
. . . 4
⊢ ((𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺) ↔ (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix 𝑁)) −
1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))) |
| 125 | 123, 124 | sylibr 234 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺)) |
| 126 | 47 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (0...𝑀)) |
| 127 | 126, 48 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (0...(𝑀 + 1))) |
| 128 | 127, 53 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → 𝑁 ∈ (0...(♯‘𝑊))) |
| 129 | 7, 128 | jca 511 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
| 130 | 129 | ex 412 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))) |
| 131 | 130 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))) |
| 132 | 131 | impcom 407 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
| 133 | 132 | 3adant3 1133 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) |
| 134 | 133, 55 | syl 17 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (♯‘(𝑊 prefix 𝑁)) = 𝑁) |
| 135 | | isclwwlkn 30046 |
. . 3
⊢ ((𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝑊 prefix 𝑁)) = 𝑁)) |
| 136 | 125, 134,
135 | sylanbrc 583 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺)) |
| 137 | 3, 136 | syl3an2 1165 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺)) |