Step |
Hyp |
Ref |
Expression |
1 |
|
swrdf1.w |
⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 ) |
2 |
|
swrdf1.m |
⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) ) |
3 |
|
swrdf1.n |
⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
4 |
|
swrdf1.1 |
⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 ) |
5 |
|
swrdrndisj.1 |
⊢ ( 𝜑 → 𝑂 ∈ ( 𝑁 ... 𝑃 ) ) |
6 |
|
swrdrndisj.2 |
⊢ ( 𝜑 → 𝑃 ∈ ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) ) |
7 |
|
swrdrn3 |
⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) = ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ) |
8 |
1 2 3 7
|
syl3anc |
⊢ ( 𝜑 → ran ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) = ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ) |
9 |
|
elfzuz |
⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) |
10 |
|
fzss1 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑁 ... 𝑃 ) ⊆ ( 0 ... 𝑃 ) ) |
11 |
3 9 10
|
3syl |
⊢ ( 𝜑 → ( 𝑁 ... 𝑃 ) ⊆ ( 0 ... 𝑃 ) ) |
12 |
11 5
|
sseldd |
⊢ ( 𝜑 → 𝑂 ∈ ( 0 ... 𝑃 ) ) |
13 |
|
fzss1 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
14 |
3 9 13
|
3syl |
⊢ ( 𝜑 → ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
15 |
14 6
|
sseldd |
⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
16 |
|
swrdrn3 |
⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑂 ∈ ( 0 ... 𝑃 ) ∧ 𝑃 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr 〈 𝑂 , 𝑃 〉 ) = ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) |
17 |
1 12 15 16
|
syl3anc |
⊢ ( 𝜑 → ran ( 𝑊 substr 〈 𝑂 , 𝑃 〉 ) = ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) |
18 |
8 17
|
ineq12d |
⊢ ( 𝜑 → ( ran ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) ∩ ran ( 𝑊 substr 〈 𝑂 , 𝑃 〉 ) ) = ( ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ∩ ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) ) |
19 |
|
df-f1 |
⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ↔ ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) ) |
20 |
19
|
simprbi |
⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → Fun ◡ 𝑊 ) |
21 |
|
imain |
⊢ ( Fun ◡ 𝑊 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ( ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ∩ ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) ) |
22 |
4 20 21
|
3syl |
⊢ ( 𝜑 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ( ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ∩ ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) ) |
23 |
|
elfzuz |
⊢ ( 𝑂 ∈ ( 𝑁 ... 𝑃 ) → 𝑂 ∈ ( ℤ≥ ‘ 𝑁 ) ) |
24 |
|
fzoss1 |
⊢ ( 𝑂 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ 𝑃 ) ) |
25 |
5 23 24
|
3syl |
⊢ ( 𝜑 → ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ 𝑃 ) ) |
26 |
|
elfzuz3 |
⊢ ( 𝑃 ∈ ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑃 ) ) |
27 |
|
fzoss2 |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑃 ) → ( 𝑁 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) |
28 |
6 26 27
|
3syl |
⊢ ( 𝜑 → ( 𝑁 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) |
29 |
25 28
|
sstrd |
⊢ ( 𝜑 → ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) |
30 |
|
sslin |
⊢ ( ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) ) |
31 |
29 30
|
syl |
⊢ ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) ) |
32 |
|
fzodisj |
⊢ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) = ∅ |
33 |
31 32
|
sseqtrdi |
⊢ ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ∅ ) |
34 |
|
ss0 |
⊢ ( ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ∅ → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) = ∅ ) |
35 |
33 34
|
syl |
⊢ ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) = ∅ ) |
36 |
35
|
imaeq2d |
⊢ ( 𝜑 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ( 𝑊 “ ∅ ) ) |
37 |
|
ima0 |
⊢ ( 𝑊 “ ∅ ) = ∅ |
38 |
36 37
|
eqtrdi |
⊢ ( 𝜑 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ∅ ) |
39 |
18 22 38
|
3eqtr2d |
⊢ ( 𝜑 → ( ran ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) ∩ ran ( 𝑊 substr 〈 𝑂 , 𝑃 〉 ) ) = ∅ ) |