Metamath Proof Explorer

Theorem wrdred1hash

Description: The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion wrdred1hash ⊢ F ∈ Word S ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 = F − 1

Proof

Step Hyp Ref Expression
1 lencl ⊢ F ∈ Word S → F ∈ ℕ 0
2 wrdf ⊢ F ∈ Word S → F : 0 ..^ F ⟶ S
3 ffn ⊢ F : 0 ..^ F ⟶ S → F Fn 0 ..^ F
4 nn0z ⊢ F ∈ ℕ 0 → F ∈ ℤ
5 fzossrbm1 ⊢ F ∈ ℤ → 0 ..^ F − 1 ⊆ 0 ..^ F
6 4 5 syl ⊢ F ∈ ℕ 0 → 0 ..^ F − 1 ⊆ 0 ..^ F
7 6 adantr ⊢ F ∈ ℕ 0 ∧ 1 ≤ F → 0 ..^ F − 1 ⊆ 0 ..^ F
8 7 adantl ⊢ F Fn 0 ..^ F ∧ F ∈ ℕ 0 ∧ 1 ≤ F → 0 ..^ F − 1 ⊆ 0 ..^ F
9 fnssresb ⊢ F Fn 0 ..^ F → F ↾ 0 ..^ F − 1 Fn 0 ..^ F − 1 ↔ 0 ..^ F − 1 ⊆ 0 ..^ F
10 9 adantr ⊢ F Fn 0 ..^ F ∧ F ∈ ℕ 0 ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 Fn 0 ..^ F − 1 ↔ 0 ..^ F − 1 ⊆ 0 ..^ F
11 8 10 mpbird ⊢ F Fn 0 ..^ F ∧ F ∈ ℕ 0 ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 Fn 0 ..^ F − 1
12 hashfn ⊢ F ↾ 0 ..^ F − 1 Fn 0 ..^ F − 1 → F ↾ 0 ..^ F − 1 = 0 ..^ F − 1
13 11 12 syl ⊢ F Fn 0 ..^ F ∧ F ∈ ℕ 0 ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 = 0 ..^ F − 1
14 1nn0 ⊢ 1 ∈ ℕ 0
15 nn0sub2 ⊢ 1 ∈ ℕ 0 ∧ F ∈ ℕ 0 ∧ 1 ≤ F → F − 1 ∈ ℕ 0
16 14 15 mp3an1 ⊢ F ∈ ℕ 0 ∧ 1 ≤ F → F − 1 ∈ ℕ 0
17 hashfzo0 ⊢ F − 1 ∈ ℕ 0 → 0 ..^ F − 1 = F − 1
18 16 17 syl ⊢ F ∈ ℕ 0 ∧ 1 ≤ F → 0 ..^ F − 1 = F − 1
19 18 adantl ⊢ F Fn 0 ..^ F ∧ F ∈ ℕ 0 ∧ 1 ≤ F → 0 ..^ F − 1 = F − 1
20 13 19 eqtrd ⊢ F Fn 0 ..^ F ∧ F ∈ ℕ 0 ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 = F − 1
21 20 ex ⊢ F Fn 0 ..^ F → F ∈ ℕ 0 ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 = F − 1
22 2 3 21 3syl ⊢ F ∈ Word S → F ∈ ℕ 0 ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 = F − 1
23 1 22 mpand ⊢ F ∈ Word S → 1 ≤ F → F ↾ 0 ..^ F − 1 = F − 1
24 23 imp ⊢ F ∈ Word S ∧ 1 ≤ F → F ↾ 0 ..^ F − 1 = F − 1