Metamath Proof Explorer

Theorem swrdwrdsymb

Description: A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022)

Ref Expression
Assertion swrdwrdsymb ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 swrdval2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) )
2 1 3expb ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) )
3 wrdf ⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
4 3 ffund ⊢ ( 𝑆 ∈ Word 𝐴 → Fun 𝑆 )
5 4 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → Fun 𝑆 )
6 5 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → Fun 𝑆 )
7 wrddm ⊢ ( 𝑆 ∈ Word 𝐴 → dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
8 elfzodifsumelfzo ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
9 8 imp ⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
10 9 adantl ⊢ ( ( dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
11 eleq2 ⊢ ( dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → ( ( 𝑥 + 𝑀 ) ∈ dom 𝑆 ↔ ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
12 11 adantr ⊢ ( ( dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝑥 + 𝑀 ) ∈ dom 𝑆 ↔ ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
13 10 12 mpbird ⊢ ( ( dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑥 + 𝑀 ) ∈ dom 𝑆 )
14 13 exp32 ⊢ ( dom 𝑆 = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝑥 + 𝑀 ) ∈ dom 𝑆 ) ) )
15 7 14 syl ⊢ ( 𝑆 ∈ Word 𝐴 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝑥 + 𝑀 ) ∈ dom 𝑆 ) ) )
16 15 imp31 ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ dom 𝑆 )
17 simpr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
18 elfzelz ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑁 ∈ ℤ )
19 18 adantl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑁 ∈ ℤ )
20 19 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑁 ∈ ℤ )
21 20 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ℤ )
22 elfzelz ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℤ )
23 22 ad2antrl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑀 ∈ ℤ )
24 23 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℤ )
25 fzoaddel2 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
26 17 21 24 25 syl3anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
27 funfvima ⊢ ( ( Fun 𝑆 ∧ ( 𝑥 + 𝑀 ) ∈ dom 𝑆 ) → ( ( 𝑥 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ∈ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ) )
28 27 imp ⊢ ( ( ( Fun 𝑆 ∧ ( 𝑥 + 𝑀 ) ∈ dom 𝑆 ) ∧ ( 𝑥 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ∈ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
29 6 16 26 28 syl21anc ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ∈ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
30 29 fmpttd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
31 fvex ⊢ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ∈ V
32 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) )
33 31 32 fnmpti ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) )
34 hashfn ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )
35 33 34 mp1i ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) )
36 fznn0sub ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
37 hashfzo0 ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) = ( 𝑁 − 𝑀 ) )
38 36 37 syl ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ♯ ‘ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) = ( 𝑁 − 𝑀 ) )
39 35 38 eqtrd ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) = ( 𝑁 − 𝑀 ) )
40 39 oveq2d ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) ) = ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
41 40 feq2d ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ) )
42 41 ad2antrl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ) )
43 30 42 mpbird ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
44 iswrdb ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ) ) ⟶ ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
45 43 44 sylibr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑀 ) ) ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
46 2 45 eqeltrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
47 46 expcom ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ) )
48 swrdnd0 ⊢ ( 𝑆 ∈ Word 𝐴 → ( ¬ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ ) )
49 wrd0 ⊢ ∅ ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) )
50 eleq1 ⊢ ( ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ → ( ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ↔ ∅ ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ) )
51 49 50 mpbiri ⊢ ( ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )
52 48 51 syl6com ⊢ ( ¬ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) ) )
53 47 52 pm2.61i ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word ( 𝑆 “ ( 𝑀 ..^ 𝑁 ) ) )