# 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 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge {U}\in \mathrm{Word}{V}\right)\wedge \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge \left({N}\le \left|{W}\right|\wedge {N}\le \left|{U}\right|\right)\right)\to \left|{W}\mathrm{substr}⟨{M},{N}⟩\right|=\left|{U}\mathrm{substr}⟨{M},{N}⟩\right|$

### Proof

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