This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdlend

Description: The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrdlend ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ → L ≤ F → W substr F L = ∅

Proof

Step Hyp Ref Expression
1 swrdval ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ → W substr F L = if F ..^ L ⊆ dom ⁡ W i ∈ 0 ..^ L − F ⟼ W ⁡ i + F ∅
2 1 adantr ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → W substr F L = if F ..^ L ⊆ dom ⁡ W i ∈ 0 ..^ L − F ⟼ W ⁡ i + F ∅
3 simpr ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → L ≤ F
4 3simpc ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ → F ∈ ℤ ∧ L ∈ ℤ
5 4 adantr ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → F ∈ ℤ ∧ L ∈ ℤ
6 fzon ⊢ F ∈ ℤ ∧ L ∈ ℤ → L ≤ F ↔ F ..^ L = ∅
7 5 6 syl ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → L ≤ F ↔ F ..^ L = ∅
8 3 7 mpbid ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → F ..^ L = ∅
9 0ss ⊢ ∅ ⊆ dom ⁡ W
10 8 9 eqsstrdi ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → F ..^ L ⊆ dom ⁡ W
11 10 iftrued ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → if F ..^ L ⊆ dom ⁡ W i ∈ 0 ..^ L − F ⟼ W ⁡ i + F ∅ = i ∈ 0 ..^ L − F ⟼ W ⁡ i + F
12 fzo0n ⊢ F ∈ ℤ ∧ L ∈ ℤ → L ≤ F ↔ 0 ..^ L − F = ∅
13 12 biimpa ⊢ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → 0 ..^ L − F = ∅
14 13 3adantl1 ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → 0 ..^ L − F = ∅
15 14 mpteq1d ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → i ∈ 0 ..^ L − F ⟼ W ⁡ i + F = i ∈ ∅ ⟼ W ⁡ i + F
16 mpt0 ⊢ i ∈ ∅ ⟼ W ⁡ i + F = ∅
17 15 16 eqtrdi ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → i ∈ 0 ..^ L − F ⟼ W ⁡ i + F = ∅
18 2 11 17 3eqtrd ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ ∧ L ≤ F → W substr F L = ∅
19 18 ex ⊢ W ∈ Word V ∧ F ∈ ℤ ∧ L ∈ ℤ → L ≤ F → W substr F L = ∅