Step | Hyp | Ref
| Expression |
1 | | pfxcl 40249 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝑌) ∈ Word 𝐴) |
2 | 1 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝑌) ∈ Word 𝐴) |
3 | | swrdcl 13271 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
4 | 3 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
5 | | ccatcl 13212 |
. . . . 5
⊢ (((𝑆 prefix 𝑌) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴) |
6 | 2, 4, 5 | syl2anc 691 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴) |
7 | | wrdf 13165 |
. . . 4
⊢ (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) ∈ Word 𝐴 → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)):(0..^(#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))))⟶𝐴) |
8 | | ffn 5958 |
. . . 4
⊢ (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)):(0..^(#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))))⟶𝐴 → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))))) |
9 | 6, 7, 8 | 3syl 18 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))))) |
10 | | ccatlen 13213 |
. . . . . . 7
⊢ (((𝑆 prefix 𝑌) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) → (#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = ((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉)))) |
11 | 2, 4, 10 | syl2anc 691 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = ((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉)))) |
12 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 𝑆 ∈ Word 𝐴) |
13 | | fzass4 12250 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ (0...(#‘𝑆)) ∧ 𝑍 ∈ (𝑌...(#‘𝑆))) ↔ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆)))) |
14 | 13 | biimpri 217 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑌 ∈ (0...(#‘𝑆)) ∧ 𝑍 ∈ (𝑌...(#‘𝑆)))) |
15 | 14 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 𝑌 ∈ (0...(#‘𝑆))) |
16 | 15 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 𝑌 ∈ (0...(#‘𝑆))) |
17 | | pfxlen 40254 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...(#‘𝑆))) → (#‘(𝑆 prefix 𝑌)) = 𝑌) |
18 | 12, 16, 17 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (#‘(𝑆 prefix 𝑌)) = 𝑌) |
19 | | swrdlen 13275 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈𝑌, 𝑍〉)) = (𝑍 − 𝑌)) |
20 | 18, 19 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉))) = (𝑌 + (𝑍 − 𝑌))) |
21 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (0...𝑍) → 𝑌 ∈ ℤ) |
22 | 21 | ad2antrl 760 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆)))) → 𝑌 ∈ ℤ) |
23 | 22 | zcnd 11359 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆)))) → 𝑌 ∈ ℂ) |
24 | 23 | 3impb 1252 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 𝑌 ∈ ℂ) |
25 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ (0...(#‘𝑆)) → 𝑍 ∈ ℤ) |
26 | 25 | ad2antll 761 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆)))) → 𝑍 ∈ ℤ) |
27 | 26 | zcnd 11359 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆)))) → 𝑍 ∈ ℂ) |
28 | 27 | 3impb 1252 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 𝑍 ∈ ℂ) |
29 | 24, 28 | pncan3d 10274 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑌 + (𝑍 − 𝑌)) = 𝑍) |
30 | 20, 29 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉))) = 𝑍) |
31 | 11, 30 | eqtrd 2644 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))) = 𝑍) |
32 | 31 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (0..^(#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)))) = (0..^𝑍)) |
33 | 32 | fneq2d 5896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^(#‘((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)))) ↔ ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^𝑍))) |
34 | 9, 33 | mpbid 221 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) Fn (0..^𝑍)) |
35 | | pfxfn 40253 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝑍) Fn (0..^𝑍)) |
36 | 35 | 3adant2 1073 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝑍) Fn (0..^𝑍)) |
37 | | simpr 476 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → 𝑥 ∈ (0..^𝑍)) |
38 | 21 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 𝑌 ∈ ℤ) |
39 | 38 | adantr 480 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → 𝑌 ∈ ℤ) |
40 | | fzospliti 12369 |
. . . . 5
⊢ ((𝑥 ∈ (0..^𝑍) ∧ 𝑌 ∈ ℤ) → (𝑥 ∈ (0..^𝑌) ∨ 𝑥 ∈ (𝑌..^𝑍))) |
41 | 37, 39, 40 | syl2anc 691 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → (𝑥 ∈ (0..^𝑌) ∨ 𝑥 ∈ (𝑌..^𝑍))) |
42 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → (𝑆 prefix 𝑌) ∈ Word 𝐴) |
43 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
44 | 18 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (0..^(#‘(𝑆 prefix 𝑌))) = (0..^𝑌)) |
45 | 44 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑥 ∈ (0..^(#‘(𝑆 prefix 𝑌))) ↔ 𝑥 ∈ (0..^𝑌))) |
46 | 45 | biimpar 501 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → 𝑥 ∈ (0..^(#‘(𝑆 prefix 𝑌)))) |
47 | | ccatval1 13214 |
. . . . . . 7
⊢ (((𝑆 prefix 𝑌) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘(𝑆 prefix 𝑌)))) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 prefix 𝑌)‘𝑥)) |
48 | 42, 43, 46, 47 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 prefix 𝑌)‘𝑥)) |
49 | 12 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → 𝑆 ∈ Word 𝐴) |
50 | 16 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → 𝑌 ∈ (0...(#‘𝑆))) |
51 | | simpr 476 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → 𝑥 ∈ (0..^𝑌)) |
52 | | pfxfv 40262 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...(#‘𝑆)) ∧ 𝑥 ∈ (0..^𝑌)) → ((𝑆 prefix 𝑌)‘𝑥) = (𝑆‘𝑥)) |
53 | 49, 50, 51, 52 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → ((𝑆 prefix 𝑌)‘𝑥) = (𝑆‘𝑥)) |
54 | 48, 53 | eqtrd 2644 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑌)) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘𝑥)) |
55 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑆 prefix 𝑌) ∈ Word 𝐴) |
56 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴) |
57 | 18, 30 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((#‘(𝑆 prefix 𝑌))..^((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉)))) = (𝑌..^𝑍)) |
58 | 57 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑥 ∈ ((#‘(𝑆 prefix 𝑌))..^((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉)))) ↔ 𝑥 ∈ (𝑌..^𝑍))) |
59 | 58 | biimpar 501 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → 𝑥 ∈ ((#‘(𝑆 prefix 𝑌))..^((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉))))) |
60 | | ccatval2 13215 |
. . . . . . 7
⊢ (((𝑆 prefix 𝑌) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑌, 𝑍〉) ∈ Word 𝐴 ∧ 𝑥 ∈ ((#‘(𝑆 prefix 𝑌))..^((#‘(𝑆 prefix 𝑌)) + (#‘(𝑆 substr 〈𝑌, 𝑍〉))))) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (#‘(𝑆 prefix 𝑌))))) |
61 | 55, 56, 59, 60 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (#‘(𝑆 prefix 𝑌))))) |
62 | 18 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (𝑥 − (#‘(𝑆 prefix 𝑌))) = (𝑥 − 𝑌)) |
63 | 62 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑥 − (#‘(𝑆 prefix 𝑌))) = (𝑥 − 𝑌)) |
64 | 38 | anim1i 590 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑌 ∈ ℤ ∧ 𝑥 ∈ (𝑌..^𝑍))) |
65 | 64 | ancomd 466 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑥 ∈ (𝑌..^𝑍) ∧ 𝑌 ∈ ℤ)) |
66 | | fzosubel 12394 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑌..^𝑍) ∧ 𝑌 ∈ ℤ) → (𝑥 − 𝑌) ∈ ((𝑌 − 𝑌)..^(𝑍 − 𝑌))) |
67 | 65, 66 | syl 17 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑥 − 𝑌) ∈ ((𝑌 − 𝑌)..^(𝑍 − 𝑌))) |
68 | 21 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ (0...𝑍) → 𝑌 ∈ ℂ) |
69 | 68 | subidd 10259 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ (0...𝑍) → (𝑌 − 𝑌) = 0) |
70 | 69 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (0...𝑍) → 0 = (𝑌 − 𝑌)) |
71 | 70 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → 0 = (𝑌 − 𝑌)) |
72 | 71 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → (0..^(𝑍 − 𝑌)) = ((𝑌 − 𝑌)..^(𝑍 − 𝑌))) |
73 | 72 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((𝑥 − 𝑌) ∈ (0..^(𝑍 − 𝑌)) ↔ (𝑥 − 𝑌) ∈ ((𝑌 − 𝑌)..^(𝑍 − 𝑌)))) |
74 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → ((𝑥 − 𝑌) ∈ (0..^(𝑍 − 𝑌)) ↔ (𝑥 − 𝑌) ∈ ((𝑌 − 𝑌)..^(𝑍 − 𝑌)))) |
75 | 67, 74 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑥 − 𝑌) ∈ (0..^(𝑍 − 𝑌))) |
76 | 63, 75 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑥 − (#‘(𝑆 prefix 𝑌))) ∈ (0..^(𝑍 − 𝑌))) |
77 | | swrdfv 13276 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ (𝑥 − (#‘(𝑆 prefix 𝑌))) ∈ (0..^(𝑍 − 𝑌))) → ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (#‘(𝑆 prefix 𝑌)))) = (𝑆‘((𝑥 − (#‘(𝑆 prefix 𝑌))) + 𝑌))) |
78 | 76, 77 | syldan 486 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → ((𝑆 substr 〈𝑌, 𝑍〉)‘(𝑥 − (#‘(𝑆 prefix 𝑌)))) = (𝑆‘((𝑥 − (#‘(𝑆 prefix 𝑌))) + 𝑌))) |
79 | 63 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → ((𝑥 − (#‘(𝑆 prefix 𝑌))) + 𝑌) = ((𝑥 − 𝑌) + 𝑌)) |
80 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑌..^𝑍) → 𝑥 ∈ ℤ) |
81 | 80 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑌..^𝑍) → 𝑥 ∈ ℂ) |
82 | 81 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → 𝑥 ∈ ℂ) |
83 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → 𝑌 ∈ ℂ) |
84 | 82, 83 | npcand 10275 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → ((𝑥 − 𝑌) + 𝑌) = 𝑥) |
85 | 79, 84 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → ((𝑥 − (#‘(𝑆 prefix 𝑌))) + 𝑌) = 𝑥) |
86 | 85 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (𝑆‘((𝑥 − (#‘(𝑆 prefix 𝑌))) + 𝑌)) = (𝑆‘𝑥)) |
87 | 61, 78, 86 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (𝑌..^𝑍)) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘𝑥)) |
88 | 54, 87 | jaodan 822 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ (𝑥 ∈ (0..^𝑌) ∨ 𝑥 ∈ (𝑌..^𝑍))) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘𝑥)) |
89 | 41, 88 | syldan 486 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = (𝑆‘𝑥)) |
90 | 12 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → 𝑆 ∈ Word 𝐴) |
91 | | simpl3 1059 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → 𝑍 ∈ (0...(#‘𝑆))) |
92 | | pfxfv 40262 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ (0...(#‘𝑆)) ∧ 𝑥 ∈ (0..^𝑍)) → ((𝑆 prefix 𝑍)‘𝑥) = (𝑆‘𝑥)) |
93 | 90, 91, 37, 92 | syl3anc 1318 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → ((𝑆 prefix 𝑍)‘𝑥) = (𝑆‘𝑥)) |
94 | 89, 93 | eqtr4d 2647 |
. 2
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) ∧ 𝑥 ∈ (0..^𝑍)) → (((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉))‘𝑥) = ((𝑆 prefix 𝑍)‘𝑥)) |
95 | 34, 36, 94 | eqfnfvd 6222 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 prefix 𝑍)) |