Metamath Proof Explorer


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