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

Metamath Proof Explorer

Theorem swrdval2

Description: Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrdval2 ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑆 ∈ Word 𝐴 )
2 elfzelz ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐹 ∈ ℤ )
3 2 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐹 ∈ ℤ )
4 elfzelz ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ℤ )
5 4 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐿 ∈ ℤ )
6 swrdval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )
7 1 3 5 6 syl3anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )
8 elfzuz ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) → 𝐹 ∈ ( ℤ≥ ‘ 0 ) )
9 8 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐹 ∈ ( ℤ≥ ‘ 0 ) )
10 fzoss1 ⊢ ( 𝐹 ∈ ( ℤ≥ ‘ 0 ) → ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ 𝐿 ) )
11 9 10 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ 𝐿 ) )
12 elfzuz3 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
13 12 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
14 fzoss2 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐿 ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
15 13 14 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
16 11 15 sstrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
17 wrddm ⊢ ( 𝑆 ∈ Word 𝐴 → dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
18 17 3ad2ant1 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
19 16 18 sseqtrrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 )
20 19 iftrued ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) )
21 7 20 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) )