Step | Hyp | Ref
| Expression |
1 | | swrdcl 14097 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴) |
3 | | swrdcl 14097 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
4 | 3 | adantr 484 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
5 | | ccatcl 14016 |
. . . . 5
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴) |
6 | 2, 4, 5 | syl2anc 587 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴) |
7 | | wrdfn 13970 |
. . . 4
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴 → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(♯‘((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))))) |
8 | 6, 7 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(♯‘((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))))) |
9 | | ccatlen 14017 |
. . . . . . 7
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) → (♯‘((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = ((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) |
10 | 2, 4, 9 | syl2anc 587 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘((𝑆 substr
〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = ((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) |
11 | | simpl 486 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑆 ∈ Word 𝐴) |
12 | | simpr1 1195 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ (0...𝑌)) |
13 | | simpr2 1196 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ (0...𝑍)) |
14 | | simpr3 1197 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ (0...(♯‘𝑆))) |
15 | | fzass4 13037 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈
(0...(♯‘𝑆))
∧ 𝑍 ∈ (𝑌...(♯‘𝑆))) ↔ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) |
16 | 15 | biimpri 231 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (𝑌 ∈ (0...(♯‘𝑆)) ∧ 𝑍 ∈ (𝑌...(♯‘𝑆)))) |
17 | 16 | simpld 498 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → 𝑌 ∈ (0...(♯‘𝑆))) |
18 | 13, 14, 17 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ (0...(♯‘𝑆))) |
19 | | swrdlen 14099 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝑋, 𝑌〉)) = (𝑌 − 𝑋)) |
20 | 11, 12, 18, 19 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘(𝑆 substr
〈𝑋, 𝑌〉)) = (𝑌 − 𝑋)) |
21 | | swrdlen 14099 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝑌, 𝑍〉)) = (𝑍 − 𝑌)) |
22 | 21 | 3adant3r1 1183 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘(𝑆 substr
〈𝑌, 𝑍〉)) = (𝑍 − 𝑌)) |
23 | 20, 22 | oveq12d 7189 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
((♯‘(𝑆 substr
〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))) = ((𝑌 − 𝑋) + (𝑍 − 𝑌))) |
24 | 13 | elfzelzd 13000 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ ℤ) |
25 | 24 | zcnd 12170 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ ℂ) |
26 | 12 | elfzelzd 13000 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ ℤ) |
27 | 26 | zcnd 12170 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ ℂ) |
28 | 14 | elfzelzd 13000 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ ℤ) |
29 | 28 | zcnd 12170 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ ℂ) |
30 | 25, 27, 29 | npncan3d 11112 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑌 − 𝑋) + (𝑍 − 𝑌)) = (𝑍 − 𝑋)) |
31 | 10, 23, 30 | 3eqtrd 2777 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘((𝑆 substr
〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = (𝑍 − 𝑋)) |
32 | 31 | oveq2d 7187 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(0..^(♯‘((𝑆
substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)))) = (0..^(𝑍 − 𝑋))) |
33 | 32 | fneq2d 6433 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(♯‘((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)))) ↔ ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(𝑍 − 𝑋)))) |
34 | 8, 33 | mpbid 235 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(𝑍 − 𝑋))) |
35 | | swrdcl 14097 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑋, 𝑍〉) ∈ Word 𝐴) |
36 | 35 | adantr 484 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑍〉) ∈ Word 𝐴) |
37 | | wrdfn 13970 |
. . . 4
⊢ ((𝑆 substr 〈𝑋, 𝑍〉) ∈ Word 𝐴 → (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(♯‘(𝑆 substr 〈𝑋, 𝑍〉)))) |
38 | 36, 37 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(♯‘(𝑆 substr 〈𝑋, 𝑍〉)))) |
39 | | fzass4 13037 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0...𝑍) ∧ 𝑌 ∈ (𝑋...𝑍)) ↔ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍))) |
40 | 39 | biimpri 231 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)) → (𝑋 ∈ (0...𝑍) ∧ 𝑌 ∈ (𝑋...𝑍))) |
41 | 40 | simpld 498 |
. . . . . . 7
⊢ ((𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)) → 𝑋 ∈ (0...𝑍)) |
42 | 12, 13, 41 | syl2anc 587 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ (0...𝑍)) |
43 | | swrdlen 14099 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝑋, 𝑍〉)) = (𝑍 − 𝑋)) |
44 | 11, 42, 14, 43 | syl3anc 1372 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘(𝑆 substr
〈𝑋, 𝑍〉)) = (𝑍 − 𝑋)) |
45 | 44 | oveq2d 7187 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(0..^(♯‘(𝑆
substr 〈𝑋, 𝑍〉))) = (0..^(𝑍 − 𝑋))) |
46 | 45 | fneq2d 6433 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(♯‘(𝑆 substr 〈𝑋, 𝑍〉))) ↔ (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(𝑍 − 𝑋)))) |
47 | 38, 46 | mpbid 235 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(𝑍 − 𝑋))) |
48 | 24, 26 | zsubcld 12174 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − 𝑋) ∈ ℤ) |
49 | 48 | anim1ci 619 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (𝑥 ∈ (0..^(𝑍 − 𝑋)) ∧ (𝑌 − 𝑋) ∈ ℤ)) |
50 | | fzospliti 13161 |
. . . . 5
⊢ ((𝑥 ∈ (0..^(𝑍 − 𝑋)) ∧ (𝑌 − 𝑋) ∈ ℤ) → (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) |
51 | 49, 50 | syl 17 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) |
52 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴) |
53 | 3 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
54 | 20 | oveq2d 7187 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(0..^(♯‘(𝑆
substr 〈𝑋, 𝑌〉))) = (0..^(𝑌 − 𝑋))) |
55 | 54 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ (0..^(♯‘(𝑆 substr 〈𝑋, 𝑌〉))) ↔ 𝑥 ∈ (0..^(𝑌 − 𝑋)))) |
56 | 55 | biimpar 481 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑥 ∈ (0..^(♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) |
57 | | ccatval1 14020 |
. . . . . . 7
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥)) |
58 | 52, 53, 56, 57 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥)) |
59 | | simpll 767 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑆 ∈ Word 𝐴) |
60 | | simplr1 1216 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑋 ∈ (0...𝑌)) |
61 | 18 | adantr 484 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑌 ∈ (0...(♯‘𝑆))) |
62 | | simpr 488 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑥 ∈ (0..^(𝑌 − 𝑋))) |
63 | | swrdfv 14100 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
64 | 59, 60, 61, 62, 63 | syl31anc 1374 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
65 | 58, 64 | eqtrd 2773 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
66 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴) |
67 | 3 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
68 | 23, 30 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
((♯‘(𝑆 substr
〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))) = (𝑍 − 𝑋)) |
69 | 20, 68 | oveq12d 7189 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
((♯‘(𝑆 substr
〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) = ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) |
70 | 69 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ ((♯‘(𝑆 substr 〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) ↔ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) |
71 | 70 | biimpar 481 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ((♯‘(𝑆 substr 〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))))) |
72 | | ccatval2 14022 |
. . . . . . 7
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴 ∧ 𝑥 ∈ ((♯‘(𝑆 substr 〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))))) |
73 | 66, 67, 71, 72 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))))) |
74 | | simpll 767 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑆 ∈ Word 𝐴) |
75 | | simplr2 1217 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑌 ∈ (0...𝑍)) |
76 | | simplr3 1218 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑍 ∈ (0...(♯‘𝑆))) |
77 | 20 | oveq2d 7187 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) = (𝑥 − (𝑌 − 𝑋))) |
78 | 77 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) = (𝑥 − (𝑌 − 𝑋))) |
79 | 30 | oveq2d 7187 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) = ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) |
80 | 79 | eleq2d 2818 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) ↔ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) |
81 | 80 | biimpar 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌)))) |
82 | 28, 24 | zsubcld 12174 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑍 − 𝑌) ∈ ℤ) |
83 | 82 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑍 − 𝑌) ∈ ℤ) |
84 | | fzosubel3 13190 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) ∧ (𝑍 − 𝑌) ∈ ℤ) → (𝑥 − (𝑌 − 𝑋)) ∈ (0..^(𝑍 − 𝑌))) |
85 | 81, 83, 84 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (𝑌 − 𝑋)) ∈ (0..^(𝑍 − 𝑌))) |
86 | 78, 85 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) ∈ (0..^(𝑍 − 𝑌))) |
87 | | swrdfv 14100 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) ∧ (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) ∈ (0..^(𝑍 − 𝑌))) → ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) = (𝑆‘((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌))) |
88 | 74, 75, 76, 86, 87 | syl31anc 1374 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) = (𝑆‘((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌))) |
89 | 77 | oveq1d 7186 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌) = ((𝑥 − (𝑌 − 𝑋)) + 𝑌)) |
90 | 89 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌) = ((𝑥 − (𝑌 − 𝑋)) + 𝑌)) |
91 | | elfzoelz 13130 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)) → 𝑥 ∈ ℤ) |
92 | 91 | zcnd 12170 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)) → 𝑥 ∈ ℂ) |
93 | 92 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ℂ) |
94 | 25, 27 | subcld 11076 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − 𝑋) ∈ ℂ) |
95 | 94 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑌 − 𝑋) ∈ ℂ) |
96 | 25 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑌 ∈ ℂ) |
97 | 93, 95, 96 | subadd23d 11098 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (𝑌 − 𝑋)) + 𝑌) = (𝑥 + (𝑌 − (𝑌 − 𝑋)))) |
98 | 25, 27 | nncand 11081 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − (𝑌 − 𝑋)) = 𝑋) |
99 | 98 | oveq2d 7187 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 + (𝑌 − (𝑌 − 𝑋))) = (𝑥 + 𝑋)) |
100 | 99 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 + (𝑌 − (𝑌 − 𝑋))) = (𝑥 + 𝑋)) |
101 | 90, 97, 100 | 3eqtrd 2777 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌) = (𝑥 + 𝑋)) |
102 | 101 | fveq2d 6679 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆‘((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌)) = (𝑆‘(𝑥 + 𝑋))) |
103 | 73, 88, 102 | 3eqtrd 2777 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
104 | 65, 103 | jaodan 957 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
105 | 51, 104 | syldan 594 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
106 | | simpll 767 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑆 ∈ Word 𝐴) |
107 | 42 | adantr 484 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑋 ∈ (0...𝑍)) |
108 | | simplr3 1218 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑍 ∈ (0...(♯‘𝑆))) |
109 | | simpr 488 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑥 ∈ (0..^(𝑍 − 𝑋))) |
110 | | swrdfv 14100 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑍〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
111 | 106, 107,
108, 109, 110 | syl31anc 1374 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑍〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
112 | 105, 111 | eqtr4d 2776 |
. 2
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑋, 𝑍〉)‘𝑥)) |
113 | 34, 47, 112 | eqfnfvd 6813 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 substr 〈𝑋, 𝑍〉)) |