Step |
Hyp |
Ref |
Expression |
1 |
|
swrdval |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr 〈 𝐹 , 𝐿 〉 ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 , ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) , ∅ ) ) |
2 |
1
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝑊 substr 〈 𝐹 , 𝐿 〉 ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 , ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) , ∅ ) ) |
3 |
|
simpr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → 𝐿 ≤ 𝐹 ) |
4 |
|
3simpc |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) |
5 |
4
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) |
6 |
|
fzon |
⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 ↔ ( 𝐹 ..^ 𝐿 ) = ∅ ) ) |
7 |
5 6
|
syl |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝐿 ≤ 𝐹 ↔ ( 𝐹 ..^ 𝐿 ) = ∅ ) ) |
8 |
3 7
|
mpbid |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝐹 ..^ 𝐿 ) = ∅ ) |
9 |
|
0ss |
⊢ ∅ ⊆ dom 𝑊 |
10 |
8 9
|
eqsstrdi |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 ) |
11 |
10
|
iftrued |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 , ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) , ∅ ) = ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) ) |
12 |
|
fzo0n |
⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 ↔ ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) ) |
13 |
12
|
biimpa |
⊢ ( ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) |
14 |
13
|
3adantl1 |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) |
15 |
14
|
mpteq1d |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) = ( 𝑖 ∈ ∅ ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) ) |
16 |
|
mpt0 |
⊢ ( 𝑖 ∈ ∅ ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) = ∅ |
17 |
15 16
|
eqtrdi |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) = ∅ ) |
18 |
2 11 17
|
3eqtrd |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝑊 substr 〈 𝐹 , 𝐿 〉 ) = ∅ ) |
19 |
18
|
ex |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 → ( 𝑊 substr 〈 𝐹 , 𝐿 〉 ) = ∅ ) ) |