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∈WordV∧F∈ℤ∧L∈ℤ→L≤F→WsubstrFL=∅

Proof

Step Hyp Ref Expression
1 swrdval ⊢W∈WordV∧F∈ℤ∧L∈ℤ→WsubstrFL=ifF..^L⊆dom⁡Wi∈0..^L−F⟼W⁡i+F∅
2 1 adantr ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→WsubstrFL=ifF..^L⊆dom⁡Wi∈0..^L−F⟼W⁡i+F∅
3 simpr ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→L≤F
4 3simpc ⊢W∈WordV∧F∈ℤ∧L∈ℤ→F∈ℤ∧L∈ℤ
5 4 adantr ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→F∈ℤ∧L∈ℤ
6 fzon ⊢F∈ℤ∧L∈ℤ→L≤F↔F..^L=∅
7 5 6 syl ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→L≤F↔F..^L=∅
8 3 7 mpbid ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→F..^L=∅
9 0ss ⊢∅⊆dom⁡W
10 8 9 eqsstrdi ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→F..^L⊆dom⁡W
11 10 iftrued ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→ifF..^L⊆dom⁡Wi∈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∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→0..^L−F=∅
15 14 mpteq1d ⊢W∈WordV∧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∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→i∈0..^L−F⟼W⁡i+F=∅
18 2 11 17 3eqtrd ⊢W∈WordV∧F∈ℤ∧L∈ℤ∧L≤F→WsubstrFL=∅
19 18 ex ⊢W∈WordV∧F∈ℤ∧L∈ℤ→L≤F→WsubstrFL=∅