| Step | Hyp | Ref
| Expression |
| 1 | | swrdcl 14683 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴) |
| 3 | | swrdcl 14683 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
| 5 | | ccatcl 14612 |
. . . . 5
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴) |
| 6 | 2, 4, 5 | syl2anc 584 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴) |
| 7 | | wrdfn 14566 |
. . . 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 14613 |
. . . . . . 7
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) → (♯‘((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = ((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) |
| 10 | 2, 4, 9 | syl2anc 584 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘((𝑆 substr
〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = ((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) |
| 11 | | simpl 482 |
. . . . . . . 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 13602 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈
(0...(♯‘𝑆))
∧ 𝑍 ∈ (𝑌...(♯‘𝑆))) ↔ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) |
| 16 | 15 | biimpri 228 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (𝑌 ∈ (0...(♯‘𝑆)) ∧ 𝑍 ∈ (𝑌...(♯‘𝑆)))) |
| 17 | 16 | simpld 494 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → 𝑌 ∈ (0...(♯‘𝑆))) |
| 18 | 13, 14, 17 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ (0...(♯‘𝑆))) |
| 19 | | swrdlen 14685 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝑋, 𝑌〉)) = (𝑌 − 𝑋)) |
| 20 | 11, 12, 18, 19 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘(𝑆 substr
〈𝑋, 𝑌〉)) = (𝑌 − 𝑋)) |
| 21 | | swrdlen 14685 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝑌, 𝑍〉)) = (𝑍 − 𝑌)) |
| 22 | 21 | 3adant3r1 1183 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘(𝑆 substr
〈𝑌, 𝑍〉)) = (𝑍 − 𝑌)) |
| 23 | 20, 22 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
((♯‘(𝑆 substr
〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))) = ((𝑌 − 𝑋) + (𝑍 − 𝑌))) |
| 24 | 13 | elfzelzd 13565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ ℤ) |
| 25 | 24 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ ℂ) |
| 26 | 12 | elfzelzd 13565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ ℤ) |
| 27 | 26 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ ℂ) |
| 28 | 14 | elfzelzd 13565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ ℤ) |
| 29 | 28 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ ℂ) |
| 30 | 25, 27, 29 | npncan3d 11656 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑌 − 𝑋) + (𝑍 − 𝑌)) = (𝑍 − 𝑋)) |
| 31 | 10, 23, 30 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘((𝑆 substr
〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = (𝑍 − 𝑋)) |
| 32 | 31 | oveq2d 7447 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(0..^(♯‘((𝑆
substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)))) = (0..^(𝑍 − 𝑋))) |
| 33 | 32 | fneq2d 6662 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(♯‘((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)))) ↔ ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(𝑍 − 𝑋)))) |
| 34 | 8, 33 | mpbid 232 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(𝑍 − 𝑋))) |
| 35 | | swrdcl 14683 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑋, 𝑍〉) ∈ Word 𝐴) |
| 36 | 35 | adantr 480 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑍〉) ∈ Word 𝐴) |
| 37 | | wrdfn 14566 |
. . . 4
⊢ ((𝑆 substr 〈𝑋, 𝑍〉) ∈ Word 𝐴 → (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(♯‘(𝑆 substr 〈𝑋, 𝑍〉)))) |
| 38 | 36, 37 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(♯‘(𝑆 substr 〈𝑋, 𝑍〉)))) |
| 39 | | fzass4 13602 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0...𝑍) ∧ 𝑌 ∈ (𝑋...𝑍)) ↔ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍))) |
| 40 | 39 | biimpri 228 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)) → (𝑋 ∈ (0...𝑍) ∧ 𝑌 ∈ (𝑋...𝑍))) |
| 41 | 40 | simpld 494 |
. . . . . . 7
⊢ ((𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)) → 𝑋 ∈ (0...𝑍)) |
| 42 | 12, 13, 41 | syl2anc 584 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ (0...𝑍)) |
| 43 | | swrdlen 14685 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝑋, 𝑍〉)) = (𝑍 − 𝑋)) |
| 44 | 11, 42, 14, 43 | syl3anc 1373 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(♯‘(𝑆 substr
〈𝑋, 𝑍〉)) = (𝑍 − 𝑋)) |
| 45 | 44 | oveq2d 7447 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(0..^(♯‘(𝑆
substr 〈𝑋, 𝑍〉))) = (0..^(𝑍 − 𝑋))) |
| 46 | 45 | fneq2d 6662 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(♯‘(𝑆 substr 〈𝑋, 𝑍〉))) ↔ (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(𝑍 − 𝑋)))) |
| 47 | 38, 46 | mpbid 232 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr 〈𝑋, 𝑍〉) Fn (0..^(𝑍 − 𝑋))) |
| 48 | 24, 26 | zsubcld 12727 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − 𝑋) ∈ ℤ) |
| 49 | 48 | anim1ci 616 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (𝑥 ∈ (0..^(𝑍 − 𝑋)) ∧ (𝑌 − 𝑋) ∈ ℤ)) |
| 50 | | fzospliti 13731 |
. . . . 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 7447 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
(0..^(♯‘(𝑆
substr 〈𝑋, 𝑌〉))) = (0..^(𝑌 − 𝑋))) |
| 55 | 54 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ (0..^(♯‘(𝑆 substr 〈𝑋, 𝑌〉))) ↔ 𝑥 ∈ (0..^(𝑌 − 𝑋)))) |
| 56 | 55 | biimpar 477 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑥 ∈ (0..^(♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) |
| 57 | | ccatval1 14615 |
. . . . . . 7
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥)) |
| 58 | 52, 53, 56, 57 | syl3anc 1373 |
. . . . . 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 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑌 ∈ (0...(♯‘𝑆))) |
| 62 | | simpr 484 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑥 ∈ (0..^(𝑌 − 𝑋))) |
| 63 | | swrdfv 14686 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 64 | 59, 60, 61, 62, 63 | syl31anc 1375 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑌〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 65 | 58, 64 | eqtrd 2777 |
. . . . 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 2777 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
((♯‘(𝑆 substr
〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))) = (𝑍 − 𝑋)) |
| 69 | 20, 68 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) →
((♯‘(𝑆 substr
〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) = ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) |
| 70 | 69 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ ((♯‘(𝑆 substr 〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉)))) ↔ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) |
| 71 | 70 | biimpar 477 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ((♯‘(𝑆 substr 〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))))) |
| 72 | | ccatval2 14616 |
. . . . . . 7
⊢ (((𝑆 substr 〈𝑋, 𝑌〉) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴 ∧ 𝑥 ∈ ((♯‘(𝑆 substr 〈𝑋, 𝑌〉))..^((♯‘(𝑆 substr 〈𝑋, 𝑌〉)) + (♯‘(𝑆 substr 〈𝑌, 𝑍〉))))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))))) |
| 73 | 66, 67, 71, 72 | syl3anc 1373 |
. . . . . 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 7447 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) = (𝑥 − (𝑌 − 𝑋))) |
| 78 | 77 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) = (𝑥 − (𝑌 − 𝑋))) |
| 79 | 30 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) = ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) |
| 80 | 79 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) ↔ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) |
| 81 | 80 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌)))) |
| 82 | 28, 24 | zsubcld 12727 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑍 − 𝑌) ∈ ℤ) |
| 83 | 82 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑍 − 𝑌) ∈ ℤ) |
| 84 | | fzosubel3 13765 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) ∧ (𝑍 − 𝑌) ∈ ℤ) → (𝑥 − (𝑌 − 𝑋)) ∈ (0..^(𝑍 − 𝑌))) |
| 85 | 81, 83, 84 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (𝑌 − 𝑋)) ∈ (0..^(𝑍 − 𝑌))) |
| 86 | 78, 85 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) ∈ (0..^(𝑍 − 𝑌))) |
| 87 | | swrdfv 14686 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) ∧ (𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) ∈ (0..^(𝑍 − 𝑌))) → ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) = (𝑆‘((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌))) |
| 88 | 74, 75, 76, 86, 87 | syl31anc 1375 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉)))) = (𝑆‘((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌))) |
| 89 | 77 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌) = ((𝑥 − (𝑌 − 𝑋)) + 𝑌)) |
| 90 | 89 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌) = ((𝑥 − (𝑌 − 𝑋)) + 𝑌)) |
| 91 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)) → 𝑥 ∈ ℤ) |
| 92 | 91 | zcnd 12723 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)) → 𝑥 ∈ ℂ) |
| 93 | 92 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ℂ) |
| 94 | 25, 27 | subcld 11620 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − 𝑋) ∈ ℂ) |
| 95 | 94 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑌 − 𝑋) ∈ ℂ) |
| 96 | 25 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑌 ∈ ℂ) |
| 97 | 93, 95, 96 | subadd23d 11642 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (𝑌 − 𝑋)) + 𝑌) = (𝑥 + (𝑌 − (𝑌 − 𝑋)))) |
| 98 | 25, 27 | nncand 11625 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − (𝑌 − 𝑋)) = 𝑋) |
| 99 | 98 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 + (𝑌 − (𝑌 − 𝑋))) = (𝑥 + 𝑋)) |
| 100 | 99 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 + (𝑌 − (𝑌 − 𝑋))) = (𝑥 + 𝑋)) |
| 101 | 90, 97, 100 | 3eqtrd 2781 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌) = (𝑥 + 𝑋)) |
| 102 | 101 | fveq2d 6910 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆‘((𝑥 − (♯‘(𝑆 substr 〈𝑋, 𝑌〉))) + 𝑌)) = (𝑆‘(𝑥 + 𝑋))) |
| 103 | 73, 88, 102 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 104 | 65, 103 | jaodan 960 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 105 | 51, 104 | syldan 591 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 106 | | simpll 767 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑆 ∈ Word 𝐴) |
| 107 | 42 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑋 ∈ (0...𝑍)) |
| 108 | | simplr3 1218 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑍 ∈ (0...(♯‘𝑆))) |
| 109 | | simpr 484 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑥 ∈ (0..^(𝑍 − 𝑋))) |
| 110 | | swrdfv 14686 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑍〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 111 | 106, 107,
108, 109, 110 | syl31anc 1375 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → ((𝑆 substr 〈𝑋, 𝑍〉)‘𝑥) = (𝑆‘(𝑥 + 𝑋))) |
| 112 | 105, 111 | eqtr4d 2780 |
. 2
⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑋, 𝑍〉)‘𝑥)) |
| 113 | 34, 47, 112 | eqfnfvd 7054 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 substr 〈𝑋, 𝑍〉)) |