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