This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrd0

Description: A subword of an empty set is always the empty set. (Contributed by AV, 31-Mar-2018) (Revised by AV, 20-Oct-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrd0 ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅

Proof

Step Hyp Ref Expression
1 opelxp ⊢ ( ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) ↔ ( ∅ ∈ V ∧ ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ) )
2 opelxp ⊢ ( ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ↔ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
3 swrdval ⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )
4 fzonlt0 ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 𝐹 < 𝐿 ↔ ( 𝐹 ..^ 𝐿 ) = ∅ ) )
5 4 biimprd ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐹 ..^ 𝐿 ) = ∅ → ¬ 𝐹 < 𝐿 ) )
6 5 con2d ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 𝐿 → ¬ ( 𝐹 ..^ 𝐿 ) = ∅ ) )
7 6 impcom ⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) = ∅ )
8 ss0 ⊢ ( ( 𝐹 ..^ 𝐿 ) ⊆ ∅ → ( 𝐹 ..^ 𝐿 ) = ∅ )
9 7 8 nsyl ⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) ⊆ ∅ )
10 dm0 ⊢ dom ∅ = ∅
11 10 a1i ⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ∅ = ∅ )
12 11 sseq2d ⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ ↔ ( 𝐹 ..^ 𝐿 ) ⊆ ∅ ) )
13 9 12 mtbird ⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ¬ ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ )
14 13 iffalsed ⊢ ( ( 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
15 ssidd ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ∅ ⊆ ∅ )
16 4 biimpac ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐹 ..^ 𝐿 ) = ∅ )
17 10 a1i ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ∅ = ∅ )
18 15 16 17 3sstr4d ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ )
19 18 iftrued ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) )
20 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
21 zre ⊢ ( 𝐹 ∈ ℤ → 𝐹 ∈ ℝ )
22 lenlt ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( 𝐿 ≤ 𝐹 ↔ ¬ 𝐹 < 𝐿 ) )
23 22 bicomd ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( ¬ 𝐹 < 𝐿 ↔ 𝐿 ≤ 𝐹 ) )
24 20 21 23 syl2anr ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 𝐹 < 𝐿 ↔ 𝐿 ≤ 𝐹 ) )
25 fzo0n ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝐹 ↔ ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) )
26 24 25 bitrd ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 𝐹 < 𝐿 ↔ ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ ) )
27 26 biimpac ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 0 ..^ ( 𝐿 − 𝐹 ) ) = ∅ )
28 27 mpteq1d ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) )
29 28 dmeqd ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = dom ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) )
30 ral0 ⊢ ∀ 𝑥 ∈ ∅ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ∈ V
31 dmmptg ⊢ ( ∀ 𝑥 ∈ ∅ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ∈ V → dom ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
32 30 31 mp1i ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
33 29 32 eqtrd ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
34 mptrel ⊢ Rel ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) )
35 reldm0 ⊢ ( Rel ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ↔ dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ) )
36 34 35 mp1i ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ↔ dom ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ ) )
37 33 36 mpbird ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) = ∅ )
38 19 37 eqtrd ⊢ ( ( ¬ 𝐹 < 𝐿 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
39 14 38 pm2.61ian ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
40 39 3adant1 ⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom ∅ , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( ∅ ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) = ∅ )
41 3 40 eqtrd ⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
42 41 3expb ⊢ ( ( ∅ ∈ V ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
43 2 42 sylan2b ⊢ ( ( ∅ ∈ V ∧ ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
44 1 43 sylbi ⊢ ( ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
45 df-substr ⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑧 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑧 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )
46 ovex ⊢ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ∈ V
47 46 mptex ⊢ ( 𝑧 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑧 + ( 1st ‘ 𝑏 ) ) ) ) ∈ V
48 0ex ⊢ ∅ ∈ V
49 47 48 ifex ⊢ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑧 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑧 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) ∈ V
50 45 49 dmmpo ⊢ dom substr = ( V × ( ℤ × ℤ ) )
51 44 50 eleq2s ⊢ ( ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ dom substr → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
52 df-ov ⊢ ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( substr ‘ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ )
53 ndmfv ⊢ ( ¬ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ dom substr → ( substr ‘ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ) = ∅ )
54 52 53 eqtrid ⊢ ( ¬ ⟨ ∅ , ⟨ 𝐹 , 𝐿 ⟩ ⟩ ∈ dom substr → ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
55 51 54 pm2.61i ⊢ ( ∅ substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅