Proof of Theorem redwlklem
Step | Hyp | Ref
| Expression |
1 | | 2mwlk 26049 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
2 | | lencl 13179 |
. . . . 5
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℕ0) |
3 | | wrdf 13165 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
4 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → 𝐹 Fn (0..^(#‘𝐹))) |
5 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℤ) |
6 | | fzossrbm1 12366 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℤ → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
8 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 1 ≤ (#‘𝐹)) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
9 | 8 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹)))
→ (0..^((#‘𝐹)
− 1)) ⊆ (0..^(#‘𝐹))) |
10 | | fnssresb 5917 |
. . . . . . . . . . 11
⊢ (𝐹 Fn (0..^(#‘𝐹)) → ((𝐹 ↾ (0..^((#‘𝐹) − 1))) Fn (0..^((#‘𝐹) − 1)) ↔
(0..^((#‘𝐹) −
1)) ⊆ (0..^(#‘𝐹)))) |
11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹)))
→ ((𝐹 ↾
(0..^((#‘𝐹) −
1))) Fn (0..^((#‘𝐹)
− 1)) ↔ (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))) |
12 | 9, 11 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹)))
→ (𝐹 ↾
(0..^((#‘𝐹) −
1))) Fn (0..^((#‘𝐹)
− 1))) |
13 | | hashfn 13025 |
. . . . . . . . 9
⊢ ((𝐹 ↾ (0..^((#‘𝐹) − 1))) Fn
(0..^((#‘𝐹) −
1)) → (#‘(𝐹
↾ (0..^((#‘𝐹)
− 1)))) = (#‘(0..^((#‘𝐹) − 1)))) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹)))
→ (#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = (#‘(0..^((#‘𝐹) − 1)))) |
15 | | 1nn0 11185 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
16 | | nn0sub2 11315 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ0 ∧ (#‘𝐹) ∈ ℕ0 ∧ 1 ≤
(#‘𝐹)) →
((#‘𝐹) − 1)
∈ ℕ0) |
17 | 15, 16 | mp3an1 1403 |
. . . . . . . . . 10
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 1 ≤ (#‘𝐹)) → ((#‘𝐹) − 1) ∈
ℕ0) |
18 | | hashfzo0 13077 |
. . . . . . . . . 10
⊢
(((#‘𝐹)
− 1) ∈ ℕ0 → (#‘(0..^((#‘𝐹) − 1))) = ((#‘𝐹) − 1)) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 1 ≤ (#‘𝐹)) → (#‘(0..^((#‘𝐹) − 1))) = ((#‘𝐹) − 1)) |
20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹)))
→ (#‘(0..^((#‘𝐹) − 1))) = ((#‘𝐹) − 1)) |
21 | 14, 20 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹)))
→ (#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1)) |
22 | 21 | ex 449 |
. . . . . 6
⊢ (𝐹 Fn (0..^(#‘𝐹)) → (((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹))
→ (#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1))) |
23 | 3, 4, 22 | 3syl 18 |
. . . . 5
⊢ (𝐹 ∈ Word dom 𝐸 → (((#‘𝐹) ∈ ℕ0
∧ 1 ≤ (#‘𝐹))
→ (#‘(𝐹 ↾
(0..^((#‘𝐹) −
1)))) = ((#‘𝐹)
− 1))) |
24 | 2, 23 | mpand 707 |
. . . 4
⊢ (𝐹 ∈ Word dom 𝐸 → (1 ≤ (#‘𝐹) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) =
((#‘𝐹) −
1))) |
25 | 24 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (1 ≤ (#‘𝐹) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1))) |
26 | 1, 25 | syl 17 |
. 2
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (1 ≤ (#‘𝐹) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1))) |
27 | 26 | imp 444 |
1
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) |