swrdsbslen

Description: Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020)

		Ref	Expression
	Assertion	swrdsbslen	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (W \in Word V \land U \in Word V)$
2		simpr2	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (M \in ℕ_{0} \land N \in ℕ_{0})$
3		simpl	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to N \leq M$
4		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⟩$
5	1 2 3 4	syl3anc	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$
6	5	fveq2d	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$
7		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
8		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
9		ltnle	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \leftrightarrow \neg N \leq M)$
10		ltle	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \to M \leq N)$
11	9 10	sylbird	$⊢ (M \in ℝ \land N \in ℝ) \to (\neg N \leq M \to M \leq N)$
12	7 8 11	syl2an	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg N \leq M \to M \leq N)$
13	12	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (\neg N \leq M \to M \leq N)$
14		simpl1l	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to W \in Word V$
15		simpl2l	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to M \in ℕ_{0}$
16		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
17		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
18	16 17	anim12i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \in ℤ \land N \in ℤ)$
19	18	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (M \in ℤ \land N \in ℤ)$
20	19	anim1i	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to ((M \in ℤ \land N \in ℤ) \land M \leq N)$
21		df-3an	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land M \leq N)$
22	20 21	sylibr	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (M \in ℤ \land N \in ℤ \land M \leq N)$
23		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
24	22 23	sylibr	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to N \in ℤ_{\geq M}$
25		simpl3l	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to N \leq \|W\|$
26		swrdlen2	$⊢ (W \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|W\|) \to \|W substr ⟨M, N⟩\| = N - M$
27	14 15 24 25 26	syl121anc	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to \|W substr ⟨M, N⟩\| = N - M$
28		simpl1r	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to U \in Word V$
29		simpl3r	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to N \leq \|U\|$
30		swrdlen2	$⊢ (U \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|U\|) \to \|U substr ⟨M, N⟩\| = N - M$
31	28 15 24 29 30	syl121anc	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to \|U substr ⟨M, N⟩\| = N - M$
32	27 31	eqtr4d	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$
33	32	ex	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (M \leq N \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|)$
34	13 33	syld	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (\neg N \leq M \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|)$
35	34	impcom	$⊢ (\neg N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$
36	6 35	pm2.61ian	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$

Metamath Proof Explorer

Theorem swrdsbslen

Proof