Proof of Theorem wrdred1hash
Step | Hyp | Ref
| Expression |
1 | | lencl 10908 |
. . 3
⊢ (𝐹 ∈ Word 𝑆 → (♯‘𝐹) ∈
ℕ0) |
2 | | wrdf 10910 |
. . . 4
⊢ (𝐹 ∈ Word 𝑆 → 𝐹:(0..^(♯‘𝐹))⟶𝑆) |
3 | | ffn 5395 |
. . . 4
⊢ (𝐹:(0..^(♯‘𝐹))⟶𝑆 → 𝐹 Fn (0..^(♯‘𝐹))) |
4 | | nn0z 9327 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℤ) |
5 | | fzossrbm1 10230 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ ℤ → (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))) |
6 | 4, 5 | syl 14 |
. . . . . . . . 9
⊢
((♯‘𝐹)
∈ ℕ0 → (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))) |
7 | 6 | ad2antrl 490 |
. . . . . . . 8
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))) |
8 | | fnssresb 5358 |
. . . . . . . . 9
⊢ (𝐹 Fn (0..^(♯‘𝐹)) → ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) Fn
(0..^((♯‘𝐹)
− 1)) ↔ (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹)))) |
9 | 8 | adantr 276 |
. . . . . . . 8
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) Fn
(0..^((♯‘𝐹)
− 1)) ↔ (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹)))) |
10 | 7, 9 | mpbird 167 |
. . . . . . 7
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) Fn
(0..^((♯‘𝐹)
− 1))) |
11 | | 0z 9318 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
12 | 4 | ad2antrl 490 |
. . . . . . . . 9
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → (♯‘𝐹) ∈ ℤ) |
13 | | peano2zm 9345 |
. . . . . . . . 9
⊢
((♯‘𝐹)
∈ ℤ → ((♯‘𝐹) − 1) ∈
ℤ) |
14 | 12, 13 | syl 14 |
. . . . . . . 8
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → ((♯‘𝐹) − 1) ∈
ℤ) |
15 | | fzofig 10493 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ ((♯‘𝐹) − 1) ∈ ℤ) →
(0..^((♯‘𝐹)
− 1)) ∈ Fin) |
16 | 11, 14, 15 | sylancr 414 |
. . . . . . 7
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → (0..^((♯‘𝐹) − 1)) ∈
Fin) |
17 | | fihashfn 10861 |
. . . . . . 7
⊢ (((𝐹 ↾
(0..^((♯‘𝐹)
− 1))) Fn (0..^((♯‘𝐹) − 1)) ∧
(0..^((♯‘𝐹)
− 1)) ∈ Fin) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) =
(♯‘(0..^((♯‘𝐹) − 1)))) |
18 | 10, 16, 17 | syl2anc 411 |
. . . . . 6
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) =
(♯‘(0..^((♯‘𝐹) − 1)))) |
19 | | 1nn0 9246 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
20 | | nn0sub2 9380 |
. . . . . . . . 9
⊢ ((1
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0 ∧ 1 ≤
(♯‘𝐹)) →
((♯‘𝐹) −
1) ∈ ℕ0) |
21 | 19, 20 | mp3an1 1335 |
. . . . . . . 8
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 1 ≤ (♯‘𝐹)) → ((♯‘𝐹) − 1) ∈
ℕ0) |
22 | | hashfzo0 10884 |
. . . . . . . 8
⊢
(((♯‘𝐹)
− 1) ∈ ℕ0 →
(♯‘(0..^((♯‘𝐹) − 1))) = ((♯‘𝐹) − 1)) |
23 | 21, 22 | syl 14 |
. . . . . . 7
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 1 ≤ (♯‘𝐹)) →
(♯‘(0..^((♯‘𝐹) − 1))) = ((♯‘𝐹) − 1)) |
24 | 23 | adantl 277 |
. . . . . 6
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) →
(♯‘(0..^((♯‘𝐹) − 1))) = ((♯‘𝐹) − 1)) |
25 | 18, 24 | eqtrd 2226 |
. . . . 5
⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹))) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) =
((♯‘𝐹) −
1)) |
26 | 25 | ex 115 |
. . . 4
⊢ (𝐹 Fn (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0
∧ 1 ≤ (♯‘𝐹)) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) =
((♯‘𝐹) −
1))) |
27 | 2, 3, 26 | 3syl 17 |
. . 3
⊢ (𝐹 ∈ Word 𝑆 → (((♯‘𝐹) ∈ ℕ0 ∧ 1 ≤
(♯‘𝐹)) →
(♯‘(𝐹 ↾
(0..^((♯‘𝐹)
− 1)))) = ((♯‘𝐹) − 1))) |
28 | 1, 27 | mpand 429 |
. 2
⊢ (𝐹 ∈ Word 𝑆 → (1 ≤ (♯‘𝐹) → (♯‘(𝐹 ↾
(0..^((♯‘𝐹)
− 1)))) = ((♯‘𝐹) − 1))) |
29 | 28 | imp 124 |
1
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹)) → (♯‘(𝐹 ↾
(0..^((♯‘𝐹)
− 1)))) = ((♯‘𝐹) − 1)) |