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

Metamath Proof Explorer

Theorem pfxnd

Description: The value of a prefix operation for a length argument larger than the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv ). (Contributed by AV, 3-May-2020)

Ref Expression
Assertion pfxnd ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W prefix L = ∅

Proof

Step Hyp Ref Expression
1 pfxval ⊢ W ∈ Word V ∧ L ∈ ℕ 0 → W prefix L = W substr 0 L
2 1 3adant3 ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W prefix L = W substr 0 L
3 simp1 ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W ∈ Word V
4 0zd ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → 0 ∈ ℤ
5 nn0z ⊢ L ∈ ℕ 0 → L ∈ ℤ
6 5 3ad2ant2 ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → L ∈ ℤ
7 3 4 6 3jca ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W ∈ Word V ∧ 0 ∈ ℤ ∧ L ∈ ℤ
8 3mix3 ⊢ W < L → 0 < 0 ∨ L ≤ 0 ∨ W < L
9 8 3ad2ant3 ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → 0 < 0 ∨ L ≤ 0 ∨ W < L
10 swrdnd ⊢ W ∈ Word V ∧ 0 ∈ ℤ ∧ L ∈ ℤ → 0 < 0 ∨ L ≤ 0 ∨ W < L → W substr 0 L = ∅
11 7 9 10 sylc ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W substr 0 L = ∅
12 2 11 eqtrd ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W prefix L = ∅