# Metamath Proof Explorer

## Theorem redwlklem

Description: Lemma for redwlk . (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion redwlklem ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to \left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)⟶{V}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left(\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to {P}:\left(0\dots \left|{F}\right|\right)⟶{V}$
2 fzossfz ${⊢}\left(0..^\left|{F}\right|\right)\subseteq \left(0\dots \left|{F}\right|\right)$
3 fssres ${⊢}\left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\wedge \left(0..^\left|{F}\right|\right)\subseteq \left(0\dots \left|{F}\right|\right)\right)\to \left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0..^\left|{F}\right|\right)⟶{V}$
4 1 2 3 sylancl ${⊢}\left(\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to \left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0..^\left|{F}\right|\right)⟶{V}$
5 4 ex ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0..^\left|{F}\right|\right)⟶{V}\right)$
6 lencl ${⊢}{F}\in \mathrm{Word}{S}\to \left|{F}\right|\in {ℕ}_{0}$
7 6 nn0zd ${⊢}{F}\in \mathrm{Word}{S}\to \left|{F}\right|\in ℤ$
8 fzoval ${⊢}\left|{F}\right|\in ℤ\to \left(0..^\left|{F}\right|\right)=\left(0\dots \left|{F}\right|-1\right)$
9 7 8 syl ${⊢}{F}\in \mathrm{Word}{S}\to \left(0..^\left|{F}\right|\right)=\left(0\dots \left|{F}\right|-1\right)$
10 9 adantr ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left(0..^\left|{F}\right|\right)=\left(0\dots \left|{F}\right|-1\right)$
11 wrdred1hash ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|=\left|{F}\right|-1$
12 oveq2 ${⊢}\left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|=\left|{F}\right|-1\to \left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)=\left(0\dots \left|{F}\right|-1\right)$
13 12 eqeq2d ${⊢}\left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|=\left|{F}\right|-1\to \left(\left(0..^\left|{F}\right|\right)=\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)↔\left(0..^\left|{F}\right|\right)=\left(0\dots \left|{F}\right|-1\right)\right)$
14 11 13 syl ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left(\left(0..^\left|{F}\right|\right)=\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)↔\left(0..^\left|{F}\right|\right)=\left(0\dots \left|{F}\right|-1\right)\right)$
15 10 14 mpbird ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left(0..^\left|{F}\right|\right)=\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)$
16 15 feq2d ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left(\left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0..^\left|{F}\right|\right)⟶{V}↔\left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)⟶{V}\right)$
17 5 16 sylibd ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\right)\to \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)⟶{V}\right)$
18 17 3impia ${⊢}\left({F}\in \mathrm{Word}{S}\wedge 1\le \left|{F}\right|\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to \left({{P}↾}_{\left(0..^\left|{F}\right|\right)}\right):\left(0\dots \left|{{F}↾}_{\left(0..^\left|{F}\right|-1\right)}\right|\right)⟶{V}$