Metamath Proof Explorer

Theorem swrdnd2

Description: Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018)

Ref Expression
Assertion swrdnd2 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ 𝐴 ∨ ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 3orass ⊢ ( ( 𝐵 ≤ 𝐴 ∨ ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ↔ ( 𝐵 ≤ 𝐴 ∨ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) )
2 pm2.24 ⊢ ( 𝐵 ≤ 𝐴 → ( ¬ 𝐵 ≤ 𝐴 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) ) )
3 swrdval ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = if ( ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 , ( 𝑥 ∈ ( 0 ..^ ( 𝐵 − 𝐴 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝐴 ) ) ) , ∅ ) )
4 3 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = if ( ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 , ( 𝑥 ∈ ( 0 ..^ ( 𝐵 − 𝐴 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝐴 ) ) ) , ∅ ) )
5 wrddm ⊢ ( 𝑊 ∈ Word 𝑉 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7 3anass ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) )
8 ssfzoulel ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐵 ≤ 𝐴 ) ) )
9 8 imp ⊢ ( ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐵 ≤ 𝐴 ) )
10 7 9 sylanbr ⊢ ( ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐵 ≤ 𝐴 ) )
11 10 con3dimp ⊢ ( ( ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 sseq2 ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 ↔ ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
13 12 notbid ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ¬ ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 ↔ ¬ ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
14 11 13 imbitrrid ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 ) )
15 14 exp5j ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ¬ 𝐵 ≤ 𝐴 → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 ) ) ) ) )
16 5 6 15 sylc ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ¬ 𝐵 ≤ 𝐴 → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 ) ) ) )
17 16 3impib ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ¬ 𝐵 ≤ 𝐴 → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 ) ) )
18 17 imp31 ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 )
19 18 iffalsed ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) ∧ ¬ 𝐵 ≤ 𝐴 ) → if ( ( 𝐴 ..^ 𝐵 ) ⊆ dom 𝑊 , ( 𝑥 ∈ ( 0 ..^ ( 𝐵 − 𝐴 ) ) ↦ ( 𝑊 ‘ ( 𝑥 + 𝐴 ) ) ) , ∅ ) = ∅ )
20 4 19 eqtrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
21 20 ex ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ¬ 𝐵 ≤ 𝐴 → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )
22 21 expcom ⊢ ( ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ¬ 𝐵 ≤ 𝐴 → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) ) )
23 22 com23 ⊢ ( ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ¬ 𝐵 ≤ 𝐴 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) ) )
24 2 23 jaoi ⊢ ( ( 𝐵 ≤ 𝐴 ∨ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ¬ 𝐵 ≤ 𝐴 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) ) )
25 swrdlend ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )
26 25 com12 ⊢ ( 𝐵 ≤ 𝐴 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )
27 24 26 pm2.61d2 ⊢ ( ( 𝐵 ≤ 𝐴 ∨ ( ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )
28 1 27 sylbi ⊢ ( ( 𝐵 ≤ 𝐴 ∨ ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )
29 28 com12 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ 𝐴 ∨ ( ♯ ‘ 𝑊 ) ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( 𝑊 substr ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )