Metamath Proof Explorer

Theorem swrdcl

Description: Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion swrdcl ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ∈ Word 𝐴 )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ∈ Word 𝐴 ↔ ∅ ∈ Word 𝐴 ) )
2 n0 ⊢ ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) )
3 df-substr ⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )
4 3 elmpocl2 ⊢ ( 𝑥 ∈ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) → ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) )
5 opelxp ⊢ ( ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ↔ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
6 4 5 sylib ⊢ ( 𝑥 ∈ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
7 6 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
8 2 7 sylbi ⊢ ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ≠ ∅ → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
9 swrdval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )
10 wrdf ⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
11 10 3ad2ant1 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
12 11 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
13 simplr ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 )
14 simpr ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
15 simpll3 ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → 𝐿 ∈ ℤ )
16 simpll2 ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → 𝐹 ∈ ℤ )
17 fzoaddel2 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ∧ 𝐿 ∈ ℤ ∧ 𝐹 ∈ ℤ ) → ( 𝑥 + 𝐹 ) ∈ ( 𝐹 ..^ 𝐿 ) )
18 14 15 16 17 syl3anc ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( 𝑥 + 𝐹 ) ∈ ( 𝐹 ..^ 𝐿 ) )
19 13 18 sseldd ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( 𝑥 + 𝐹 ) ∈ dom 𝑆 )
20 12 fdmd ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
21 19 20 eleqtrd ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( 𝑥 + 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
22 12 21 ffvelcdmd ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ∈ 𝐴 )
23 22 fmpttd ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) : ( 0 ..^ ( 𝐿 − 𝐹 ) ) ⟶ 𝐴 )
24 iswrdi ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) : ( 0 ..^ ( 𝐿 − 𝐹 ) ) ⟶ 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) ∈ Word 𝐴 )
25 23 24 syl ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) ∈ Word 𝐴 )
26 wrd0 ⊢ ∅ ∈ Word 𝐴
27 26 a1i ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) → ∅ ∈ Word 𝐴 )
28 25 27 ifclda ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) ∈ Word 𝐴 )
29 9 28 eqeltrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ∈ Word 𝐴 )
30 29 3expb ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ∈ Word 𝐴 )
31 8 30 sylan2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ≠ ∅ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ∈ Word 𝐴 )
32 26 a1i ⊢ ( 𝑆 ∈ Word 𝐴 → ∅ ∈ Word 𝐴 )
33 1 31 32 pm2.61ne ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ∈ Word 𝐴 )