Step | Hyp | Ref
| Expression |
1 | | swrdval2 14008 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑥 + 𝑀)))) |
2 | 1 | rneqd 5808 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) = ran (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑥 + 𝑀)))) |
3 | | eqidd 2822 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (♯‘𝑊) = (♯‘𝑊)) |
4 | | simpl1 1187 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑊 ∈ Word 𝑉) |
5 | 3, 4 | wrdfd 30612 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑊:(0..^(♯‘𝑊))⟶𝑉) |
6 | 5 | ffund 6518 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → Fun 𝑊) |
7 | | elfzuz3 12906 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝑁)) |
8 | 7 | 3ad2ant3 1131 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈
(ℤ≥‘𝑁)) |
9 | 8 | adantr 483 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (♯‘𝑊) ∈ (ℤ≥‘𝑁)) |
10 | | fzoss2 13066 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝑊))) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (0..^𝑁) ⊆ (0..^(♯‘𝑊))) |
12 | | elfzuz 12905 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈
(ℤ≥‘0)) |
13 | 12 | 3ad2ant2 1130 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑀 ∈
(ℤ≥‘0)) |
14 | 13 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈
(ℤ≥‘0)) |
15 | | fzoss1 13065 |
. . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝑀..^𝑁) ⊆ (0..^𝑁)) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑀..^𝑁) ⊆ (0..^𝑁)) |
17 | | simpr 487 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑥 ∈ (0..^(𝑁 − 𝑀))) |
18 | | fzssz 12910 |
. . . . . . . . . 10
⊢
(0...(♯‘𝑊)) ⊆ ℤ |
19 | | simpl3 1189 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ (0...(♯‘𝑊))) |
20 | 18, 19 | sseldi 3965 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ ℤ) |
21 | | fzssz 12910 |
. . . . . . . . . 10
⊢
(0...𝑁) ⊆
ℤ |
22 | | simpl2 1188 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ (0...𝑁)) |
23 | 21, 22 | sseldi 3965 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ ℤ) |
24 | | fzoaddel2 13094 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑥 + 𝑀) ∈ (𝑀..^𝑁)) |
25 | 17, 20, 23, 24 | syl3anc 1367 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (𝑀..^𝑁)) |
26 | 16, 25 | sseldd 3968 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝑁)) |
27 | 11, 26 | sseldd 3968 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^(♯‘𝑊))) |
28 | | wrddm 13869 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(♯‘𝑊))) |
29 | 28 | 3ad2ant1 1129 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → dom 𝑊 = (0..^(♯‘𝑊))) |
30 | 29 | adantr 483 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → dom 𝑊 = (0..^(♯‘𝑊))) |
31 | 27, 30 | eleqtrrd 2916 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ dom 𝑊) |
32 | | fvelrn 6844 |
. . . . 5
⊢ ((Fun
𝑊 ∧ (𝑥 + 𝑀) ∈ dom 𝑊) → (𝑊‘(𝑥 + 𝑀)) ∈ ran 𝑊) |
33 | 6, 31, 32 | syl2anc 586 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑊‘(𝑥 + 𝑀)) ∈ ran 𝑊) |
34 | 33 | ralrimiva 3182 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ∀𝑥 ∈ (0..^(𝑁 − 𝑀))(𝑊‘(𝑥 + 𝑀)) ∈ ran 𝑊) |
35 | | eqid 2821 |
. . . 4
⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑥 + 𝑀))) |
36 | 35 | rnmptss 6886 |
. . 3
⊢
(∀𝑥 ∈
(0..^(𝑁 − 𝑀))(𝑊‘(𝑥 + 𝑀)) ∈ ran 𝑊 → ran (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑥 + 𝑀))) ⊆ ran 𝑊) |
37 | 34, 36 | syl 17 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑥 + 𝑀))) ⊆ ran 𝑊) |
38 | 2, 37 | eqsstrd 4005 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ ran 𝑊) |