Theorem swrdlen2

Description: Length of an extracted subword. (Contributed by AV, 5-May-2020)

	Ref	Expression
Assertion	swrdlen2	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝑆 ∈ Word 𝑉 )
2		simpl	⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐹 ∈ ℕ0 )
3		eluznn0	⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐿 ∈ ℕ0 )
4		eluzle	⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) → 𝐹 ≤ 𝐿 )
5	4	adantl	⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐹 ≤ 𝐿 )
6	2 3 5	3jca	⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
7	6	3ad2ant2	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
8		elfz2nn0	⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) ↔ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
9	7 8	sylibr	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐹 ∈ ( 0 ... 𝐿 ) )
10	3	3ad2ant2	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ℕ0 )
11		lencl	⊢ ( 𝑆 ∈ Word 𝑉 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
12	11	3ad2ant1	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
13		simp3	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ≤ ( ♯ ‘ 𝑆 ) )
14	10 12 13	3jca	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
15		elfz2nn0	⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
16	14 15	sylibr	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
17		swrdlen	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )
18	1 9 16 17	syl3anc	⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )