Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑖 ∈ (0..^(𝑁 − 𝑀))) |
2 | | simpl3 1193 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ (0...(♯‘𝑊))) |
3 | 2 | elfzelzd 13442 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ ℤ) |
4 | | simpl2 1192 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ (0...𝑁)) |
5 | 4 | elfzelzd 13442 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ ℤ) |
6 | | fzoaddel2 13628 |
. . . . . 6
⊢ ((𝑖 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁)) |
7 | 1, 3, 5, 6 | syl3anc 1371 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁)) |
8 | | simpr 485 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀..^𝑁)) |
9 | | simpl2 1192 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ (0...𝑁)) |
10 | 9 | elfzelzd 13442 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ) |
11 | 10 | zcnd 12608 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℂ) |
12 | | simpl3 1193 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑁 ∈ (0...(♯‘𝑊))) |
13 | 12 | elfzelzd 13442 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℤ) |
14 | 13 | zcnd 12608 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℂ) |
15 | 11, 14 | pncan3d 11515 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑀 + (𝑁 − 𝑀)) = 𝑁) |
16 | 15 | oveq2d 7373 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑀..^(𝑀 + (𝑁 − 𝑀))) = (𝑀..^𝑁)) |
17 | 8, 16 | eleqtrrd 2841 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀..^(𝑀 + (𝑁 − 𝑀)))) |
18 | 13, 10 | zsubcld 12612 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑁 − 𝑀) ∈ ℤ) |
19 | | fzosubel3 13633 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝑀..^(𝑀 + (𝑁 − 𝑀))) ∧ (𝑁 − 𝑀) ∈ ℤ) → (𝑗 − 𝑀) ∈ (0..^(𝑁 − 𝑀))) |
20 | 17, 18, 19 | syl2anc 584 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 − 𝑀) ∈ (0..^(𝑁 − 𝑀))) |
21 | | simpr 485 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑖 = (𝑗 − 𝑀)) → 𝑖 = (𝑗 − 𝑀)) |
22 | 21 | oveq1d 7372 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑖 = (𝑗 − 𝑀)) → (𝑖 + 𝑀) = ((𝑗 − 𝑀) + 𝑀)) |
23 | 22 | eqeq2d 2747 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑖 = (𝑗 − 𝑀)) → (𝑗 = (𝑖 + 𝑀) ↔ 𝑗 = ((𝑗 − 𝑀) + 𝑀))) |
24 | | fzossz 13592 |
. . . . . . . . . 10
⊢ (𝑀..^𝑁) ⊆ ℤ |
25 | 24, 8 | sselid 3942 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℤ) |
26 | 25 | zcnd 12608 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℂ) |
27 | 26, 11 | npcand 11516 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑗 − 𝑀) + 𝑀) = 𝑗) |
28 | 27 | eqcomd 2742 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 = ((𝑗 − 𝑀) + 𝑀)) |
29 | 20, 23, 28 | rspcedvd 3583 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → ∃𝑖 ∈ (0..^(𝑁 − 𝑀))𝑗 = (𝑖 + 𝑀)) |
30 | | eqcom 2743 |
. . . . . 6
⊢ (𝑦 = (𝑊‘𝑗) ↔ (𝑊‘𝑗) = 𝑦) |
31 | | simpr 485 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → 𝑗 = (𝑖 + 𝑀)) |
32 | 31 | fveq2d 6846 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → (𝑊‘𝑗) = (𝑊‘(𝑖 + 𝑀))) |
33 | 32 | eqeq2d 2747 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → (𝑦 = (𝑊‘𝑗) ↔ 𝑦 = (𝑊‘(𝑖 + 𝑀)))) |
34 | 30, 33 | bitr3id 284 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → ((𝑊‘𝑗) = 𝑦 ↔ 𝑦 = (𝑊‘(𝑖 + 𝑀)))) |
35 | 7, 29, 34 | rexxfrd 5364 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (∃𝑗 ∈ (𝑀..^𝑁)(𝑊‘𝑗) = 𝑦 ↔ ∃𝑖 ∈ (0..^(𝑁 − 𝑀))𝑦 = (𝑊‘(𝑖 + 𝑀)))) |
36 | | eqid 2736 |
. . . . 5
⊢ (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))) = (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))) |
37 | | fvex 6855 |
. . . . 5
⊢ (𝑊‘(𝑖 + 𝑀)) ∈ V |
38 | 36, 37 | elrnmpti 5915 |
. . . 4
⊢ (𝑦 ∈ ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))) ↔ ∃𝑖 ∈ (0..^(𝑁 − 𝑀))𝑦 = (𝑊‘(𝑖 + 𝑀))) |
39 | 35, 38 | bitr4di 288 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (∃𝑗 ∈ (𝑀..^𝑁)(𝑊‘𝑗) = 𝑦 ↔ 𝑦 ∈ ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))))) |
40 | | wrdf 14407 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → 𝑊:(0..^(♯‘𝑊))⟶𝑉) |
41 | 40 | 3ad2ant1 1133 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑊:(0..^(♯‘𝑊))⟶𝑉) |
42 | 41 | ffnd 6669 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑊 Fn (0..^(♯‘𝑊))) |
43 | | elfzuz 13437 |
. . . . . . 7
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈
(ℤ≥‘0)) |
44 | 43 | 3ad2ant2 1134 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑀 ∈
(ℤ≥‘0)) |
45 | | fzoss1 13599 |
. . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝑀..^𝑁) ⊆ (0..^𝑁)) |
46 | 44, 45 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑀..^𝑁) ⊆ (0..^𝑁)) |
47 | | elfzuz3 13438 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝑁)) |
48 | 47 | 3ad2ant3 1135 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈
(ℤ≥‘𝑁)) |
49 | | fzoss2 13600 |
. . . . . 6
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝑊))) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (0..^𝑁) ⊆
(0..^(♯‘𝑊))) |
51 | 46, 50 | sstrd 3954 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑀..^𝑁) ⊆ (0..^(♯‘𝑊))) |
52 | 42, 51 | fvelimabd 6915 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑦 ∈ (𝑊 “ (𝑀..^𝑁)) ↔ ∃𝑗 ∈ (𝑀..^𝑁)(𝑊‘𝑗) = 𝑦)) |
53 | | swrdval2 14534 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀)))) |
54 | 53 | rneqd 5893 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) = ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀)))) |
55 | 54 | eleq2d 2823 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑦 ∈ ran (𝑊 substr 〈𝑀, 𝑁〉) ↔ 𝑦 ∈ ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))))) |
56 | 39, 52, 55 | 3bitr4rd 311 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑦 ∈ ran (𝑊 substr 〈𝑀, 𝑁〉) ↔ 𝑦 ∈ (𝑊 “ (𝑀..^𝑁)))) |
57 | 56 | eqrdv 2734 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) = (𝑊 “ (𝑀..^𝑁))) |