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

Metamath Proof Explorer

Theorem swrdsb0eq

Description: Two subwords with the same bounds are equal if the range is not valid. (Contributed by AV, 4-May-2020)

Ref Expression
Assertion swrdsb0eq ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑊 ∈ Word 𝑉 )
2 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
3 2 ad2antrl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℤ )
4 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
5 4 ad2antll ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℤ )
6 swrdlend ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ ) )
7 1 3 5 6 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 ≤ 𝑀 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ ) )
8 7 3impia ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ )
9 simplr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑈 ∈ Word 𝑉 )
10 swrdlend ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 → ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ ) )
11 9 3 5 10 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 ≤ 𝑀 → ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ ) )
12 11 3impia ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ∅ )
13 8 12 eqtr4d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )