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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )

Proof

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 ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )