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