Metamath Proof Explorer

Theorem swrdsbslen

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

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

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) )
2 simpr2 ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
3 simpl ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → 𝑁 ≤ 𝑀 )
4 swrdsb0eq ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
5 1 2 3 4 syl3anc ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
6 5 fveq2d ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
7 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
8 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
9 ltnle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀 ) )
10 ltle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 → 𝑀 ≤ 𝑁 ) )
11 9 10 sylbird ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
12 7 8 11 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
13 12 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
14 simpl1l ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑊 ∈ Word 𝑉 )
15 simpl2l ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
16 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
17 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
18 16 17 anim12i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
19 18 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
20 19 anim1i ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) )
21 df-3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) )
22 20 21 sylibr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
23 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
24 22 23 sylibr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
25 simpl3l ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ≤ ( ♯ ‘ 𝑊 ) )
26 swrdlen2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
27 14 15 24 25 26 syl121anc ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
28 simpl1r ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑈 ∈ Word 𝑉 )
29 simpl3r ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ≤ ( ♯ ‘ 𝑈 ) )
30 swrdlen2 ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) → ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
31 28 15 24 29 30 syl121anc ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
32 27 31 eqtr4d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 ≤ 𝑁 ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
33 32 ex ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑀 ≤ 𝑁 → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) )
34 13 33 syld ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ¬ 𝑁 ≤ 𝑀 → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) )
35 34 impcom ⊢ ( ( ¬ 𝑁 ≤ 𝑀 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
36 6 35 pm2.61ian ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ♯ ‘ ( 𝑈 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )