This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdlen

Description: Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion swrdlen ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ∈ V
2 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) )
3 1 2 fnmpti ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) )
4 swrdval2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) )
5 4 fneq1d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) )
6 3 5 mpbiri ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
7 hashfn ⊢ ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( ♯ ‘ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) )
8 6 7 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( ♯ ‘ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) )
9 fznn0sub ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → ( 𝐿 − 𝐹 ) ∈ ℕ0 )
10 9 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐿 − 𝐹 ) ∈ ℕ0 )
11 hashfzo0 ⊢ ( ( 𝐿 − 𝐹 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) = ( 𝐿 − 𝐹 ) )
12 10 11 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) = ( 𝐿 − 𝐹 ) )
13 8 12 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )