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	syl6eq	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) = ∅ )
18	2 11 17	3eqtrd	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ 𝐹 ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
19	18	ex	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )