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 ⟨ 𝑀 , 𝑁 ⟩ ) )