Metamath Proof Explorer

Theorem swrdnd

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

Proof

Step Hyp Ref Expression
1 3orcomb ⊢ ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ↔ ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ∨ 𝐿 ≤ 𝐹 ) )
2 df-3or ⊢ ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ∨ 𝐿 ≤ 𝐹 ) ↔ ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∨ 𝐿 ≤ 𝐹 ) )
3 1 2 bitri ⊢ ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ↔ ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∨ 𝐿 ≤ 𝐹 ) )
4 swrdlend ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
5 4 com12 ⊢ ( 𝐿 ≤ 𝐹 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
6 swrdval ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 , ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) , ∅ ) )
7 6 adantl ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 , ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) , ∅ ) )
8 zre ⊢ ( 𝐹 ∈ ℤ → 𝐹 ∈ ℝ )
9 0red ⊢ ( 𝐹 ∈ ℤ → 0 ∈ ℝ )
10 8 9 ltnled ⊢ ( 𝐹 ∈ ℤ → ( 𝐹 < 0 ↔ ¬ 0 ≤ 𝐹 ) )
11 10 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 0 ↔ ¬ 0 ≤ 𝐹 ) )
12 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
13 12 nn0red ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
14 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
15 13 14 anim12i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
16 15 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
17 ltnle ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( ♯ ‘ 𝑊 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
18 16 17 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
19 11 18 orbi12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ↔ ( ¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
20 19 biimpcd ⊢ ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
21 20 adantr ⊢ ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
22 21 imp ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
23 ianor ⊢ ( ¬ ( 0 ≤ 𝐹 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ↔ ( ¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
24 22 23 sylibr ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 0 ≤ 𝐹 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
25 3simpc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
26 12 nn0zd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
27 0z ⊢ 0 ∈ ℤ
28 26 27 jctil ⊢ ( 𝑊 ∈ Word 𝑉 → ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) )
29 28 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) )
30 ltnle ⊢ ( ( 𝐹 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹 ) )
31 8 14 30 syl2an ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹 ) )
32 31 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹 ) )
33 32 biimprcd ⊢ ( ¬ 𝐿 ≤ 𝐹 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐹 < 𝐿 ) )
34 33 adantl ⊢ ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐹 < 𝐿 ) )
35 34 imp ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝐹 < 𝐿 )
36 ssfzo12bi ⊢ ( ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) ∧ 𝐹 < 𝐿 ) → ( ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 0 ≤ 𝐹 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
37 25 29 35 36 syl2an23an ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 0 ≤ 𝐹 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
38 24 37 mtbird ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 wrddm ⊢ ( 𝑊 ∈ Word 𝑉 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
40 39 sseq2d ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 ↔ ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
41 40 notbid ⊢ ( 𝑊 ∈ Word 𝑉 → ( ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 ↔ ¬ ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
42 41 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 ↔ ¬ ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
43 42 adantl ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 ↔ ¬ ( 𝐹 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
44 38 43 mpbird ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 )
45 44 iffalsed ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑊 , ( 𝑖 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑊 ‘ ( 𝑖 + 𝐹 ) ) ) , ∅ ) = ∅ )
46 7 45 eqtrd ⊢ ( ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∧ ¬ 𝐿 ≤ 𝐹 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
47 46 exp31 ⊢ ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) → ( ¬ 𝐿 ≤ 𝐹 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
48 47 impcom ⊢ ( ( ¬ 𝐿 ≤ 𝐹 ∧ ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
49 5 48 jaoi3 ⊢ ( ( 𝐿 ≤ 𝐹 ∨ ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
50 49 orcoms ⊢ ( ( ( 𝐹 < 0 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) ∨ 𝐿 ≤ 𝐹 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
51 3 50 sylbi ⊢ ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
52 51 com12 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑊 ) < 𝐿 ) → ( 𝑊 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )