Metamath Proof Explorer

Theorem swrdrn2

Description: The range of a subword is a subset of the range of that word. Stronger version of swrdrn . (Contributed by Thierry Arnoux, 12-Dec-2023)

Ref Expression
Assertion swrdrn2 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ ran 𝑊 )

Proof

Step Hyp Ref Expression
1 swrdval2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ) )
2 1 rneqd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ran ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ) )
3 eqidd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
4 simpl1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑊 ∈ Word 𝑉 )
5 3 4 wrdfd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
6 5 ffund ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → Fun 𝑊 )
7 elfzuz3 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
8 7 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
9 8 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
10 fzoss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 9 10 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 elfzuz ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
13 12 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
14 13 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
15 fzoss1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
16 14 15 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
17 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
18 fzssz ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℤ
19 simpl3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
20 18 19 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ℤ )
21 fzssz ⊢ ( 0 ... 𝑁 ) ⊆ ℤ
22 simpl2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
23 21 22 sseldi ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℤ )
24 fzoaddel2 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
25 17 20 23 24 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 𝑀 ..^ 𝑁 ) )
26 16 25 sseldd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ 𝑁 ) )
27 11 26 sseldd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
28 wrddm ⊢ ( 𝑊 ∈ Word 𝑉 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 28 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
30 29 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
31 27 30 eleqtrrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ dom 𝑊 )
32 fvelrn ⊢ ( ( Fun 𝑊 ∧ ( 𝑥 + 𝑀 ) ∈ dom 𝑊 ) → ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ∈ ran 𝑊 )
33 6 31 32 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ∈ ran 𝑊 )
34 33 ralrimiva ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ∈ ran 𝑊 )
35 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) )
36 35 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ∈ ran 𝑊 → ran ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ) ⊆ ran 𝑊 )
37 34 36 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑥 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝑀 ) ) ) ⊆ ran 𝑊 )
38 2 37 eqsstrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ ran 𝑊 )