| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pfxcl |
⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ) |
| 2 |
|
swrdcl |
⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) |
| 3 |
|
ccatcl |
⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 ) |
| 4 |
1 2 3
|
syl2anc |
⊢ ( 𝑆 ∈ Word 𝐴 → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 ) |
| 5 |
|
wrdfn |
⊢ ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ∈ Word 𝐴 → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) |
| 6 |
4 5
|
syl |
⊢ ( 𝑆 ∈ Word 𝐴 → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) |
| 7 |
6
|
adantr |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) |
| 8 |
|
ccatlen |
⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) |
| 9 |
1 2 8
|
syl2anc |
⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) |
| 10 |
9
|
adantr |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) |
| 11 |
|
fzass4 |
⊢ ( ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) |
| 12 |
11
|
biimpri |
⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 ... ( ♯ ‘ 𝑆 ) ) ) ) |
| 13 |
12
|
simpld |
⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) |
| 14 |
|
pfxlen |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) = 𝑌 ) |
| 15 |
13 14
|
sylan2 |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) = 𝑌 ) |
| 16 |
|
swrdlen |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑌 ) ) |
| 17 |
16
|
3expb |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑍 − 𝑌 ) ) |
| 18 |
15 17
|
oveq12d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = ( 𝑌 + ( 𝑍 − 𝑌 ) ) ) |
| 19 |
|
elfzelz |
⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → 𝑌 ∈ ℤ ) |
| 20 |
19
|
zcnd |
⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → 𝑌 ∈ ℂ ) |
| 21 |
|
elfzelz |
⊢ ( 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑍 ∈ ℤ ) |
| 22 |
21
|
zcnd |
⊢ ( 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑍 ∈ ℂ ) |
| 23 |
|
pncan3 |
⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ ) → ( 𝑌 + ( 𝑍 − 𝑌 ) ) = 𝑍 ) |
| 24 |
20 22 23
|
syl2an |
⊢ ( ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑌 + ( 𝑍 − 𝑌 ) ) = 𝑍 ) |
| 25 |
24
|
adantl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑌 + ( 𝑍 − 𝑌 ) ) = 𝑍 ) |
| 26 |
10 18 25
|
3eqtrd |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = 𝑍 ) |
| 27 |
26
|
oveq2d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) = ( 0 ..^ 𝑍 ) ) |
| 28 |
27
|
fneq2d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ↔ ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ 𝑍 ) ) ) |
| 29 |
7 28
|
mpbid |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) Fn ( 0 ..^ 𝑍 ) ) |
| 30 |
|
pfxfn |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝑍 ) Fn ( 0 ..^ 𝑍 ) ) |
| 31 |
30
|
adantrl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 prefix 𝑍 ) Fn ( 0 ..^ 𝑍 ) ) |
| 32 |
|
id |
⊢ ( 𝑥 ∈ ( 0 ..^ 𝑍 ) → 𝑥 ∈ ( 0 ..^ 𝑍 ) ) |
| 33 |
19
|
ad2antrl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ℤ ) |
| 34 |
|
fzospliti |
⊢ ( ( 𝑥 ∈ ( 0 ..^ 𝑍 ) ∧ 𝑌 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ 𝑌 ) ∨ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) ) |
| 35 |
32 33 34
|
syl2anr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑌 ) ∨ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) ) |
| 36 |
1
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ) |
| 37 |
2
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) |
| 38 |
15
|
oveq2d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) = ( 0 ..^ 𝑌 ) ) |
| 39 |
38
|
eleq2d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ↔ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) ) |
| 40 |
39
|
biimpar |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) |
| 41 |
|
ccatval1 |
⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) ) |
| 42 |
36 37 40 41
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) ) |
| 43 |
|
simpl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑆 ∈ Word 𝐴 ) |
| 44 |
13
|
adantl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) |
| 45 |
|
id |
⊢ ( 𝑥 ∈ ( 0 ..^ 𝑌 ) → 𝑥 ∈ ( 0 ..^ 𝑌 ) ) |
| 46 |
|
pfxfv |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 47 |
43 44 45 46
|
syl2an3an |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( 𝑆 prefix 𝑌 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 48 |
42 47
|
eqtrd |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑌 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 49 |
1
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ) |
| 50 |
2
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ) |
| 51 |
18 25
|
eqtrd |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) = 𝑍 ) |
| 52 |
15 51
|
oveq12d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) = ( 𝑌 ..^ 𝑍 ) ) |
| 53 |
52
|
eleq2d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ↔ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) ) |
| 54 |
53
|
biimpar |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) |
| 55 |
|
ccatval2 |
⊢ ( ( ( 𝑆 prefix 𝑌 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ..^ ( ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) ) |
| 56 |
49 50 54 55
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) ) |
| 57 |
|
id |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) |
| 58 |
57
|
3expb |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) |
| 59 |
15
|
oveq2d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) = ( 𝑥 − 𝑌 ) ) |
| 60 |
59
|
adantr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) = ( 𝑥 − 𝑌 ) ) |
| 61 |
|
id |
⊢ ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) → 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) |
| 62 |
|
fzosubel |
⊢ ( ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ∧ 𝑌 ∈ ℤ ) → ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ) |
| 63 |
61 33 62
|
syl2anr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ) |
| 64 |
20
|
subidd |
⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → ( 𝑌 − 𝑌 ) = 0 ) |
| 65 |
64
|
oveq1d |
⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) = ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) |
| 66 |
65
|
eleq2d |
⊢ ( 𝑌 ∈ ( 0 ... 𝑍 ) → ( ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ↔ ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) ) |
| 67 |
66
|
ad2antrl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ↔ ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) ) |
| 68 |
67
|
adantr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − 𝑌 ) ∈ ( ( 𝑌 − 𝑌 ) ..^ ( 𝑍 − 𝑌 ) ) ↔ ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) ) |
| 69 |
63 68
|
mpbid |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − 𝑌 ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) |
| 70 |
60 69
|
eqeltrd |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) |
| 71 |
|
swrdfv |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ∈ ( 0 ..^ ( 𝑍 − 𝑌 ) ) ) → ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) = ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) ) ) |
| 72 |
58 70 71
|
syl2an2r |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) ) = ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) ) ) |
| 73 |
59
|
oveq1d |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) = ( ( 𝑥 − 𝑌 ) + 𝑌 ) ) |
| 74 |
73
|
adantr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) = ( ( 𝑥 − 𝑌 ) + 𝑌 ) ) |
| 75 |
|
elfzoelz |
⊢ ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) → 𝑥 ∈ ℤ ) |
| 76 |
75
|
zcnd |
⊢ ( 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) → 𝑥 ∈ ℂ ) |
| 77 |
20
|
ad2antrl |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ℂ ) |
| 78 |
|
npcan |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑥 − 𝑌 ) + 𝑌 ) = 𝑥 ) |
| 79 |
76 77 78
|
syl2anr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − 𝑌 ) + 𝑌 ) = 𝑥 ) |
| 80 |
74 79
|
eqtrd |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) = 𝑥 ) |
| 81 |
80
|
fveq2d |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( 𝑆 ‘ ( ( 𝑥 − ( ♯ ‘ ( 𝑆 prefix 𝑌 ) ) ) + 𝑌 ) ) = ( 𝑆 ‘ 𝑥 ) ) |
| 82 |
56 72 81
|
3eqtrd |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 83 |
48 82
|
jaodan |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑌 ) ∨ 𝑥 ∈ ( 𝑌 ..^ 𝑍 ) ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 84 |
35 83
|
syldan |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 85 |
|
pfxfv |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 86 |
85
|
3expa |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 87 |
86
|
adantlrl |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
| 88 |
84 87
|
eqtr4d |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑍 ) ) → ( ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) ‘ 𝑥 ) = ( ( 𝑆 prefix 𝑍 ) ‘ 𝑥 ) ) |
| 89 |
29 31 88
|
eqfnfvd |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑆 prefix 𝑍 ) ) |
| 90 |
89
|
3impb |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... 𝑍 ) ∧ 𝑍 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , 𝑍 ⟩ ) ) = ( 𝑆 prefix 𝑍 ) ) |