Step | Hyp | Ref
| Expression |
1 | | eleq1 2689 |
. 2
⊢ ((𝑆 substr 〈𝐹, 𝐿〉) = ∅ → ((𝑆 substr 〈𝐹, 𝐿〉) ∈ Word 𝐴 ↔ ∅ ∈ Word 𝐴)) |
2 | | n0 3931 |
. . . 4
⊢ ((𝑆 substr 〈𝐹, 𝐿〉) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆 substr 〈𝐹, 𝐿〉)) |
3 | | df-substr 13303 |
. . . . . . 7
⊢ substr =
(𝑠 ∈ V, 𝑏 ∈ (ℤ ×
ℤ) ↦ if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅)) |
4 | 3 | elmpt2cl2 6878 |
. . . . . 6
⊢ (𝑥 ∈ (𝑆 substr 〈𝐹, 𝐿〉) → 〈𝐹, 𝐿〉 ∈ (ℤ ×
ℤ)) |
5 | | opelxp 5146 |
. . . . . 6
⊢
(〈𝐹, 𝐿〉 ∈ (ℤ ×
ℤ) ↔ (𝐹 ∈
ℤ ∧ 𝐿 ∈
ℤ)) |
6 | 4, 5 | sylib 208 |
. . . . 5
⊢ (𝑥 ∈ (𝑆 substr 〈𝐹, 𝐿〉) → (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) |
7 | 6 | exlimiv 1858 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ (𝑆 substr 〈𝐹, 𝐿〉) → (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) |
8 | 2, 7 | sylbi 207 |
. . 3
⊢ ((𝑆 substr 〈𝐹, 𝐿〉) ≠ ∅ → (𝐹 ∈ ℤ ∧ 𝐿 ∈
ℤ)) |
9 | | swrdval 13417 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) |
10 | | wrdf 13310 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → 𝑆:(0..^(#‘𝑆))⟶𝐴) |
11 | 10 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝑆:(0..^(#‘𝑆))⟶𝐴) |
12 | 11 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → 𝑆:(0..^(#‘𝑆))⟶𝐴) |
13 | | simplr 792 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → (𝐹..^𝐿) ⊆ dom 𝑆) |
14 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → 𝑥 ∈ (0..^(𝐿 − 𝐹))) |
15 | | simpll3 1102 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → 𝐿 ∈ ℤ) |
16 | | simpll2 1101 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → 𝐹 ∈ ℤ) |
17 | | fzoaddel2 12523 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0..^(𝐿 − 𝐹)) ∧ 𝐿 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝑥 + 𝐹) ∈ (𝐹..^𝐿)) |
18 | 14, 15, 16, 17 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → (𝑥 + 𝐹) ∈ (𝐹..^𝐿)) |
19 | 13, 18 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → (𝑥 + 𝐹) ∈ dom 𝑆) |
20 | | fdm 6051 |
. . . . . . . . . . 11
⊢ (𝑆:(0..^(#‘𝑆))⟶𝐴 → dom 𝑆 = (0..^(#‘𝑆))) |
21 | 12, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → dom 𝑆 = (0..^(#‘𝑆))) |
22 | 19, 21 | eleqtrd 2703 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → (𝑥 + 𝐹) ∈ (0..^(#‘𝑆))) |
23 | 12, 22 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐹))) → (𝑆‘(𝑥 + 𝐹)) ∈ 𝐴) |
24 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) |
25 | 23, 24 | fmptd 6385 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) → (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))):(0..^(𝐿 − 𝐹))⟶𝐴) |
26 | | iswrdi 13309 |
. . . . . . 7
⊢ ((𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))):(0..^(𝐿 − 𝐹))⟶𝐴 → (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) ∈ Word 𝐴) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐹..^𝐿) ⊆ dom 𝑆) → (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) ∈ Word 𝐴) |
28 | | wrd0 13330 |
. . . . . . 7
⊢ ∅
∈ Word 𝐴 |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ ¬ (𝐹..^𝐿) ⊆ dom 𝑆) → ∅ ∈ Word 𝐴) |
30 | 27, 29 | ifclda 4120 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅) ∈ Word 𝐴) |
31 | 9, 30 | eqeltrd 2701 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) ∈ Word 𝐴) |
32 | 31 | 3expb 1266 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑆 substr 〈𝐹, 𝐿〉) ∈ Word 𝐴) |
33 | 8, 32 | sylan2 491 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑆 substr 〈𝐹, 𝐿〉) ≠ ∅) → (𝑆 substr 〈𝐹, 𝐿〉) ∈ Word 𝐴) |
34 | 28 | a1i 11 |
. 2
⊢ (𝑆 ∈ Word 𝐴 → ∅ ∈ Word 𝐴) |
35 | 1, 33, 34 | pm2.61ne 2879 |
1
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝐹, 𝐿〉) ∈ Word 𝐴) |