| Step | Hyp | Ref
| Expression |
| 1 | | swrdval2 14684 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝑀, 𝑁〉) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))) |
| 2 | 1 | 3expb 1121 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑀, 𝑁〉) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))) |
| 3 | | wrdf 14557 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → 𝑆:(0..^(♯‘𝑆))⟶𝐴) |
| 4 | 3 | ffund 6740 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Word 𝐴 → Fun 𝑆) |
| 5 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → Fun 𝑆) |
| 6 | 5 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → Fun 𝑆) |
| 7 | | wrddm 14559 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Word 𝐴 → dom 𝑆 = (0..^(♯‘𝑆))) |
| 8 | | elfzodifsumelfzo 13770 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (𝑥 + 𝑀) ∈ (0..^(♯‘𝑆)))) |
| 9 | 8 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^(♯‘𝑆))) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((dom
𝑆 =
(0..^(♯‘𝑆))
∧ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀)))) → (𝑥 + 𝑀) ∈ (0..^(♯‘𝑆))) |
| 11 | | eleq2 2830 |
. . . . . . . . . . . . 13
⊢ (dom
𝑆 =
(0..^(♯‘𝑆))
→ ((𝑥 + 𝑀) ∈ dom 𝑆 ↔ (𝑥 + 𝑀) ∈ (0..^(♯‘𝑆)))) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((dom
𝑆 =
(0..^(♯‘𝑆))
∧ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀)))) → ((𝑥 + 𝑀) ∈ dom 𝑆 ↔ (𝑥 + 𝑀) ∈ (0..^(♯‘𝑆)))) |
| 13 | 10, 12 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((dom
𝑆 =
(0..^(♯‘𝑆))
∧ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀)))) → (𝑥 + 𝑀) ∈ dom 𝑆) |
| 14 | 13 | exp32 420 |
. . . . . . . . . 10
⊢ (dom
𝑆 =
(0..^(♯‘𝑆))
→ ((𝑀 ∈
(0...𝑁) ∧ 𝑁 ∈
(0...(♯‘𝑆)))
→ (𝑥 ∈
(0..^(𝑁 − 𝑀)) → (𝑥 + 𝑀) ∈ dom 𝑆))) |
| 15 | 7, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑆 ∈ Word 𝐴 → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (𝑥 + 𝑀) ∈ dom 𝑆))) |
| 16 | 15 | imp31 417 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ dom 𝑆) |
| 17 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑥 ∈ (0..^(𝑁 − 𝑀))) |
| 18 | | elfzelz 13564 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(0...(♯‘𝑆))
→ 𝑁 ∈
ℤ) |
| 19 | 18 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → 𝑁 ∈ ℤ) |
| 20 | 19 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → 𝑁 ∈ ℤ) |
| 21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ ℤ) |
| 22 | | elfzelz 13564 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ) |
| 23 | 22 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → 𝑀 ∈ ℤ) |
| 24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ ℤ) |
| 25 | | fzoaddel2 13759 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑥 + 𝑀) ∈ (𝑀..^𝑁)) |
| 26 | 17, 21, 24, 25 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (𝑀..^𝑁)) |
| 27 | | funfvima 7250 |
. . . . . . . . 9
⊢ ((Fun
𝑆 ∧ (𝑥 + 𝑀) ∈ dom 𝑆) → ((𝑥 + 𝑀) ∈ (𝑀..^𝑁) → (𝑆‘(𝑥 + 𝑀)) ∈ (𝑆 “ (𝑀..^𝑁)))) |
| 28 | 27 | imp 406 |
. . . . . . . 8
⊢ (((Fun
𝑆 ∧ (𝑥 + 𝑀) ∈ dom 𝑆) ∧ (𝑥 + 𝑀) ∈ (𝑀..^𝑁)) → (𝑆‘(𝑥 + 𝑀)) ∈ (𝑆 “ (𝑀..^𝑁))) |
| 29 | 6, 16, 26, 28 | syl21anc 838 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑆‘(𝑥 + 𝑀)) ∈ (𝑆 “ (𝑀..^𝑁))) |
| 30 | 29 | fmpttd 7135 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(𝑁 − 𝑀))⟶(𝑆 “ (𝑀..^𝑁))) |
| 31 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑆‘(𝑥 + 𝑀)) ∈ V |
| 32 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))) |
| 33 | 31, 32 | fnmpti 6711 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))) Fn (0..^(𝑁 − 𝑀)) |
| 34 | | hashfn 14414 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))) Fn (0..^(𝑁 − 𝑀)) → (♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))) = (♯‘(0..^(𝑁 − 𝑀)))) |
| 35 | 33, 34 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝑁) → (♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))) = (♯‘(0..^(𝑁 − 𝑀)))) |
| 36 | | fznn0sub 13596 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → (𝑁 − 𝑀) ∈
ℕ0) |
| 37 | | hashfzo0 14469 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝑀) ∈ ℕ0 →
(♯‘(0..^(𝑁
− 𝑀))) = (𝑁 − 𝑀)) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝑁) → (♯‘(0..^(𝑁 − 𝑀))) = (𝑁 − 𝑀)) |
| 39 | 35, 38 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...𝑁) → (♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))) = (𝑁 − 𝑀)) |
| 40 | 39 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...𝑁) → (0..^(♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))))) = (0..^(𝑁 − 𝑀))) |
| 41 | 40 | feq2d 6722 |
. . . . . . 7
⊢ (𝑀 ∈ (0...𝑁) → ((𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))))⟶(𝑆 “ (𝑀..^𝑁)) ↔ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(𝑁 − 𝑀))⟶(𝑆 “ (𝑀..^𝑁)))) |
| 42 | 41 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → ((𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))))⟶(𝑆 “ (𝑀..^𝑁)) ↔ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(𝑁 − 𝑀))⟶(𝑆 “ (𝑀..^𝑁)))) |
| 43 | 30, 42 | mpbird 257 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))))⟶(𝑆 “ (𝑀..^𝑁))) |
| 44 | | iswrdb 14558 |
. . . . 5
⊢ ((𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))) ∈ Word (𝑆 “ (𝑀..^𝑁)) ↔ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))):(0..^(♯‘(𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀)))))⟶(𝑆 “ (𝑀..^𝑁))) |
| 45 | 43, 44 | sylibr 234 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑆‘(𝑥 + 𝑀))) ∈ Word (𝑆 “ (𝑀..^𝑁))) |
| 46 | 2, 45 | eqeltrd 2841 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁))) |
| 47 | 46 | expcom 413 |
. 2
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁)))) |
| 48 | | swrdnd0 14695 |
. . 3
⊢ (𝑆 ∈ Word 𝐴 → (¬ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝑀, 𝑁〉) = ∅)) |
| 49 | | wrd0 14577 |
. . . 4
⊢ ∅
∈ Word (𝑆 “
(𝑀..^𝑁)) |
| 50 | | eleq1 2829 |
. . . 4
⊢ ((𝑆 substr 〈𝑀, 𝑁〉) = ∅ → ((𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁)) ↔ ∅ ∈ Word (𝑆 “ (𝑀..^𝑁)))) |
| 51 | 49, 50 | mpbiri 258 |
. . 3
⊢ ((𝑆 substr 〈𝑀, 𝑁〉) = ∅ → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁))) |
| 52 | 48, 51 | syl6com 37 |
. 2
⊢ (¬
(𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑆))) → (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁)))) |
| 53 | 47, 52 | pm2.61i 182 |
1
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁))) |