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 ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) )

Proof

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