# Metamath Proof Explorer

## Theorem 2clwwlklem

Description: Lemma for clwwnonrepclwwnon and extwwlkfab . (Contributed by Alexander van der Vekens, 18-Sep-2018) (Revised by AV, 10-May-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Assertion 2clwwlklem ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\left(0\right)={W}\left(0\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 1 clwwlknwrd ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
3 ige3m2fz ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2\in \left(1\dots {N}\right)$
4 3 adantl ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {N}\in {ℤ}_{\ge 3}\right)\to {N}-2\in \left(1\dots {N}\right)$
5 clwwlknlen ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left|{W}\right|={N}$
6 5 oveq2d ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left(1\dots \left|{W}\right|\right)=\left(1\dots {N}\right)$
7 6 eleq2d ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left({N}-2\in \left(1\dots \left|{W}\right|\right)↔{N}-2\in \left(1\dots {N}\right)\right)$
8 7 adantr ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({N}-2\in \left(1\dots \left|{W}\right|\right)↔{N}-2\in \left(1\dots {N}\right)\right)$
9 4 8 mpbird ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {N}\in {ℤ}_{\ge 3}\right)\to {N}-2\in \left(1\dots \left|{W}\right|\right)$
10 pfxfv0 ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {N}-2\in \left(1\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\left(0\right)={W}\left(0\right)$
11 2 9 10 syl2an2r ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\left(0\right)={W}\left(0\right)$