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 ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )