Metamath Proof Explorer

Theorem swrdfv2

Description: A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020)

Ref Expression
Assertion swrdfv2 ( ( ( 𝑆 ∈ 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 anim1i ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
11 10 3adant1 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
12 lencl ⊢ ( 𝑆 ∈ Word 𝑉 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
13 12 3ad2ant1 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
14 fznn0 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) )
15 13 14 syl ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) )
16 11 15 mpbird ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
17 1 9 16 3jca ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
18 17 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
19 nn0cn ⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℂ )
20 eluzelcn ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) → 𝐿 ∈ ℂ )
21 pncan3 ⊢ ( ( 𝐹 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐹 + ( 𝐿 − 𝐹 ) ) = 𝐿 )
22 19 20 21 syl2an ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → ( 𝐹 + ( 𝐿 − 𝐹 ) ) = 𝐿 )
23 22 eqcomd ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐿 = ( 𝐹 + ( 𝐿 − 𝐹 ) ) )
24 23 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 = ( 𝐹 + ( 𝐿 − 𝐹 ) ) )
25 24 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐹 ..^ 𝐿 ) = ( 𝐹 ..^ ( 𝐹 + ( 𝐿 − 𝐹 ) ) ) )
26 25 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ↔ 𝑋 ∈ ( 𝐹 ..^ ( 𝐹 + ( 𝐿 − 𝐹 ) ) ) ) )
27 26 biimpa ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → 𝑋 ∈ ( 𝐹 ..^ ( 𝐹 + ( 𝐿 − 𝐹 ) ) ) )
28 eluzelz ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) → 𝐿 ∈ ℤ )
29 28 adantl ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐿 ∈ ℤ )
30 nn0z ⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℤ )
31 30 adantr ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐹 ∈ ℤ )
32 29 31 zsubcld ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → ( 𝐿 − 𝐹 ) ∈ ℤ )
33 32 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐿 − 𝐹 ) ∈ ℤ )
34 33 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( 𝐿 − 𝐹 ) ∈ ℤ )
35 fzosubel3 ⊢ ( ( 𝑋 ∈ ( 𝐹 ..^ ( 𝐹 + ( 𝐿 − 𝐹 ) ) ) ∧ ( 𝐿 − 𝐹 ) ∈ ℤ ) → ( 𝑋 − 𝐹 ) ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
36 27 34 35 syl2anc ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( 𝑋 − 𝐹 ) ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
37 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ ( 𝑋 − 𝐹 ) ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ ( 𝑋 − 𝐹 ) ) = ( 𝑆 ‘ ( ( 𝑋 − 𝐹 ) + 𝐹 ) ) )
38 18 36 37 syl2anc ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ ( 𝑋 − 𝐹 ) ) = ( 𝑆 ‘ ( ( 𝑋 − 𝐹 ) + 𝐹 ) ) )
39 elfzoelz ⊢ ( 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) → 𝑋 ∈ ℤ )
40 39 zcnd ⊢ ( 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) → 𝑋 ∈ ℂ )
41 19 adantr ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐹 ∈ ℂ )
42 41 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐹 ∈ ℂ )
43 npcan ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝐹 ∈ ℂ ) → ( ( 𝑋 − 𝐹 ) + 𝐹 ) = 𝑋 )
44 40 42 43 syl2anr ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( ( 𝑋 − 𝐹 ) + 𝐹 ) = 𝑋 )
45 44 fveq2d ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( 𝑆 ‘ ( ( 𝑋 − 𝐹 ) + 𝐹 ) ) = ( 𝑆 ‘ 𝑋 ) )
46 38 45 eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 𝐹 ..^ 𝐿 ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ ( 𝑋 − 𝐹 ) ) = ( 𝑆 ‘ 𝑋 ) )