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	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to W \in Word V$
2		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
3	2	ad2antrl	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to M \in ℤ$
4		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
5	4	ad2antll	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to N \in ℤ$
6		swrdlend	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (N \leq M \to W substr ⟨M, N⟩ = \emptyset)$
7	1 3 5 6	syl3anc	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq M \to W substr ⟨M, N⟩ = \emptyset)$
8	7	3impia	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to W substr ⟨M, N⟩ = \emptyset$
9		simplr	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to U \in Word V$
10		swrdlend	$⊢ (U \in Word V \land M \in ℤ \land N \in ℤ) \to (N \leq M \to U substr ⟨M, N⟩ = \emptyset)$
11	9 3 5 10	syl3anc	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq M \to U substr ⟨M, N⟩ = \emptyset)$
12	11	3impia	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to U substr ⟨M, N⟩ = \emptyset$
13	8 12	eqtr4d	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$

Metamath Proof Explorer