# Metamath Proof Explorer

## Theorem wwlksubclwwlk

Description: Any prefix of a word representing a closed walk represents a walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 28-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion wwlksubclwwlk ${⊢}\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {X}\mathrm{prefix}{M}\in \left(\left({M}-1\right)\mathrm{WWalksN}{G}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
3 1 2 clwwlknp ${⊢}{X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({X}\right),{X}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
4 pfxcl ${⊢}{X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to {X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
5 4 adantr ${⊢}\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\to {X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
6 5 ad2antrr ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to {X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
7 nnz ${⊢}{M}\in ℕ\to {M}\in ℤ$
8 eluzp1m1 ${⊢}\left({M}\in ℤ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge {M}}$
9 8 ex ${⊢}{M}\in ℤ\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}-1\in {ℤ}_{\ge {M}}\right)$
10 7 9 syl ${⊢}{M}\in ℕ\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}-1\in {ℤ}_{\ge {M}}\right)$
11 peano2zm ${⊢}{M}\in ℤ\to {M}-1\in ℤ$
12 7 11 syl ${⊢}{M}\in ℕ\to {M}-1\in ℤ$
13 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
14 13 lem1d ${⊢}{M}\in ℕ\to {M}-1\le {M}$
15 eluzuzle ${⊢}\left({M}-1\in ℤ\wedge {M}-1\le {M}\right)\to \left({N}-1\in {ℤ}_{\ge {M}}\to {N}-1\in {ℤ}_{\ge \left({M}-1\right)}\right)$
16 12 14 15 syl2anc ${⊢}{M}\in ℕ\to \left({N}-1\in {ℤ}_{\ge {M}}\to {N}-1\in {ℤ}_{\ge \left({M}-1\right)}\right)$
17 10 16 syld ${⊢}{M}\in ℕ\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}-1\in {ℤ}_{\ge \left({M}-1\right)}\right)$
18 17 imp ${⊢}\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge \left({M}-1\right)}$
19 fzoss2 ${⊢}{N}-1\in {ℤ}_{\ge \left({M}-1\right)}\to \left(0..^{M}-1\right)\subseteq \left(0..^{N}-1\right)$
20 18 19 syl ${⊢}\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left(0..^{M}-1\right)\subseteq \left(0..^{N}-1\right)$
21 20 adantl ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left(0..^{M}-1\right)\subseteq \left(0..^{N}-1\right)$
22 ssralv ${⊢}\left(0..^{M}-1\right)\subseteq \left(0..^{N}-1\right)\to \left(\forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
23 21 22 syl ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left(\forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
24 simpll ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to {X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
25 24 adantr ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to {X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
26 eluz2 ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}↔\left({M}+1\in ℤ\wedge {N}\in ℤ\wedge {M}+1\le {N}\right)$
27 13 adantr ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {M}\in ℝ$
28 peano2re ${⊢}{M}\in ℝ\to {M}+1\in ℝ$
29 13 28 syl ${⊢}{M}\in ℕ\to {M}+1\in ℝ$
30 29 adantr ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {M}+1\in ℝ$
31 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
32 31 ad2antrl ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {N}\in ℝ$
33 13 lep1d ${⊢}{M}\in ℕ\to {M}\le {M}+1$
34 33 adantr ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {M}\le {M}+1$
35 simpr ${⊢}\left({N}\in ℤ\wedge {M}+1\le {N}\right)\to {M}+1\le {N}$
36 35 adantl ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {M}+1\le {N}$
37 27 30 32 34 36 letrd ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {M}\le {N}$
38 nnnn0 ${⊢}{M}\in ℕ\to {M}\in {ℕ}_{0}$
39 38 ad2antrr ${⊢}\left(\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\wedge {M}\le {N}\right)\to {M}\in {ℕ}_{0}$
40 simpr ${⊢}\left({M}\in ℕ\wedge {N}\in ℤ\right)\to {N}\in ℤ$
41 40 adantr ${⊢}\left(\left({M}\in ℕ\wedge {N}\in ℤ\right)\wedge {M}\le {N}\right)\to {N}\in ℤ$
42 0red ${⊢}\left({M}\in ℕ\wedge {N}\in ℤ\right)\to 0\in ℝ$
43 13 adantr ${⊢}\left({M}\in ℕ\wedge {N}\in ℤ\right)\to {M}\in ℝ$
44 31 adantl ${⊢}\left({M}\in ℕ\wedge {N}\in ℤ\right)\to {N}\in ℝ$
45 42 43 44 3jca ${⊢}\left({M}\in ℕ\wedge {N}\in ℤ\right)\to \left(0\in ℝ\wedge {M}\in ℝ\wedge {N}\in ℝ\right)$
46 45 adantr ${⊢}\left(\left({M}\in ℕ\wedge {N}\in ℤ\right)\wedge {M}\le {N}\right)\to \left(0\in ℝ\wedge {M}\in ℝ\wedge {N}\in ℝ\right)$
47 38 nn0ge0d ${⊢}{M}\in ℕ\to 0\le {M}$
48 47 adantr ${⊢}\left({M}\in ℕ\wedge {N}\in ℤ\right)\to 0\le {M}$
49 48 anim1i ${⊢}\left(\left({M}\in ℕ\wedge {N}\in ℤ\right)\wedge {M}\le {N}\right)\to \left(0\le {M}\wedge {M}\le {N}\right)$
50 letr ${⊢}\left(0\in ℝ\wedge {M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(0\le {M}\wedge {M}\le {N}\right)\to 0\le {N}\right)$
51 46 49 50 sylc ${⊢}\left(\left({M}\in ℕ\wedge {N}\in ℤ\right)\wedge {M}\le {N}\right)\to 0\le {N}$
52 elnn0z ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℤ\wedge 0\le {N}\right)$
53 41 51 52 sylanbrc ${⊢}\left(\left({M}\in ℕ\wedge {N}\in ℤ\right)\wedge {M}\le {N}\right)\to {N}\in {ℕ}_{0}$
54 53 adantlrr ${⊢}\left(\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\wedge {M}\le {N}\right)\to {N}\in {ℕ}_{0}$
55 simpr ${⊢}\left(\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\wedge {M}\le {N}\right)\to {M}\le {N}$
56 39 54 55 3jca ${⊢}\left(\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\wedge {M}\le {N}\right)\to \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)$
57 37 56 mpdan ${⊢}\left({M}\in ℕ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)$
58 57 expcom ${⊢}\left({N}\in ℤ\wedge {M}+1\le {N}\right)\to \left({M}\in ℕ\to \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\right)$
59 58 3adant1 ${⊢}\left({M}+1\in ℤ\wedge {N}\in ℤ\wedge {M}+1\le {N}\right)\to \left({M}\in ℕ\to \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\right)$
60 26 59 sylbi ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to \left({M}\in ℕ\to \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\right)$
61 60 impcom ${⊢}\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)$
62 elfz2nn0 ${⊢}{M}\in \left(0\dots {N}\right)↔\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)$
63 61 62 sylibr ${⊢}\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {M}\in \left(0\dots {N}\right)$
64 63 adantl ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to {M}\in \left(0\dots {N}\right)$
65 oveq2 ${⊢}\left|{X}\right|={N}\to \left(0\dots \left|{X}\right|\right)=\left(0\dots {N}\right)$
66 65 eleq2d ${⊢}\left|{X}\right|={N}\to \left({M}\in \left(0\dots \left|{X}\right|\right)↔{M}\in \left(0\dots {N}\right)\right)$
67 66 adantl ${⊢}\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\to \left({M}\in \left(0\dots \left|{X}\right|\right)↔{M}\in \left(0\dots {N}\right)\right)$
68 67 adantr ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left({M}\in \left(0\dots \left|{X}\right|\right)↔{M}\in \left(0\dots {N}\right)\right)$
69 64 68 mpbird ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to {M}\in \left(0\dots \left|{X}\right|\right)$
70 69 adantr ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to {M}\in \left(0\dots \left|{X}\right|\right)$
71 eluz2 ${⊢}{M}\in {ℤ}_{\ge \left({M}-1\right)}↔\left({M}-1\in ℤ\wedge {M}\in ℤ\wedge {M}-1\le {M}\right)$
72 12 7 14 71 syl3anbrc ${⊢}{M}\in ℕ\to {M}\in {ℤ}_{\ge \left({M}-1\right)}$
73 fzoss2 ${⊢}{M}\in {ℤ}_{\ge \left({M}-1\right)}\to \left(0..^{M}-1\right)\subseteq \left(0..^{M}\right)$
74 72 73 syl ${⊢}{M}\in ℕ\to \left(0..^{M}-1\right)\subseteq \left(0..^{M}\right)$
75 74 sseld ${⊢}{M}\in ℕ\to \left({i}\in \left(0..^{M}-1\right)\to {i}\in \left(0..^{M}\right)\right)$
76 75 ad2antrl ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left({i}\in \left(0..^{M}-1\right)\to {i}\in \left(0..^{M}\right)\right)$
77 76 imp ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to {i}\in \left(0..^{M}\right)$
78 pfxfv ${⊢}\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {M}\in \left(0\dots \left|{X}\right|\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({X}\mathrm{prefix}{M}\right)\left({i}\right)={X}\left({i}\right)$
79 25 70 77 78 syl3anc ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to \left({X}\mathrm{prefix}{M}\right)\left({i}\right)={X}\left({i}\right)$
80 79 eqcomd ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to {X}\left({i}\right)=\left({X}\mathrm{prefix}{M}\right)\left({i}\right)$
81 fzonn0p1p1 ${⊢}{i}\in \left(0..^{M}-1\right)\to {i}+1\in \left(0..^{M}-1+1\right)$
82 nncn ${⊢}{M}\in ℕ\to {M}\in ℂ$
83 npcan1 ${⊢}{M}\in ℂ\to {M}-1+1={M}$
84 82 83 syl ${⊢}{M}\in ℕ\to {M}-1+1={M}$
85 84 oveq2d ${⊢}{M}\in ℕ\to \left(0..^{M}-1+1\right)=\left(0..^{M}\right)$
86 85 eleq2d ${⊢}{M}\in ℕ\to \left({i}+1\in \left(0..^{M}-1+1\right)↔{i}+1\in \left(0..^{M}\right)\right)$
87 81 86 syl5ib ${⊢}{M}\in ℕ\to \left({i}\in \left(0..^{M}-1\right)\to {i}+1\in \left(0..^{M}\right)\right)$
88 87 ad2antrl ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left({i}\in \left(0..^{M}-1\right)\to {i}+1\in \left(0..^{M}\right)\right)$
89 88 imp ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to {i}+1\in \left(0..^{M}\right)$
90 pfxfv ${⊢}\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {M}\in \left(0\dots \left|{X}\right|\right)\wedge {i}+1\in \left(0..^{M}\right)\right)\to \left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)={X}\left({i}+1\right)$
91 25 70 89 90 syl3anc ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to \left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)={X}\left({i}+1\right)$
92 91 eqcomd ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to {X}\left({i}+1\right)=\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)$
93 80 92 preq12d ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to \left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}=\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}$
94 93 eleq1d ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\wedge {i}\in \left(0..^{M}-1\right)\right)\to \left(\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)↔\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
95 94 ralbidva ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left(\forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)↔\forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
96 23 95 sylibd ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left(\forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
97 96 impancom ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
98 97 imp ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)$
99 24 69 jca ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {M}\in \left(0\dots \left|{X}\right|\right)\right)$
100 99 adantlr ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {M}\in \left(0\dots \left|{X}\right|\right)\right)$
101 pfxlen ${⊢}\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {M}\in \left(0\dots \left|{X}\right|\right)\right)\to \left|{X}\mathrm{prefix}{M}\right|={M}$
102 100 101 syl ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left|{X}\mathrm{prefix}{M}\right|={M}$
103 102 oveq1d ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left|{X}\mathrm{prefix}{M}\right|-1={M}-1$
104 103 oveq2d ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)=\left(0..^{M}-1\right)$
105 104 raleqdv ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)↔\forall {i}\in \left(0..^{M}-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
106 98 105 mpbird ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)$
107 24 69 101 syl2anc ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left|{X}\mathrm{prefix}{M}\right|={M}$
108 84 eqcomd ${⊢}{M}\in ℕ\to {M}={M}-1+1$
109 108 ad2antrl ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to {M}={M}-1+1$
110 107 109 eqtrd ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left|{X}\mathrm{prefix}{M}\right|={M}-1+1$
111 110 adantlr ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left|{X}\mathrm{prefix}{M}\right|={M}-1+1$
112 6 106 111 3jca ${⊢}\left(\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)\to \left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)$
113 112 ex ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)\right)$
114 113 3adant3 ${⊢}\left(\left({X}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{X}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{X}\left({i}\right),{X}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({X}\right),{X}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)\right)$
115 3 114 syl ${⊢}{X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)\right)$
116 115 impcom ${⊢}\left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\wedge {X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to \left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)$
117 nnm1nn0 ${⊢}{M}\in ℕ\to {M}-1\in {ℕ}_{0}$
118 117 ad2antrr ${⊢}\left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\wedge {X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to {M}-1\in {ℕ}_{0}$
119 1 2 iswwlksnx ${⊢}{M}-1\in {ℕ}_{0}\to \left({X}\mathrm{prefix}{M}\in \left(\left({M}-1\right)\mathrm{WWalksN}{G}\right)↔\left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)\right)$
120 118 119 syl ${⊢}\left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\wedge {X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to \left({X}\mathrm{prefix}{M}\in \left(\left({M}-1\right)\mathrm{WWalksN}{G}\right)↔\left({X}\mathrm{prefix}{M}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{X}\mathrm{prefix}{M}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({X}\mathrm{prefix}{M}\right)\left({i}\right),\left({X}\mathrm{prefix}{M}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left|{X}\mathrm{prefix}{M}\right|={M}-1+1\right)\right)$
121 116 120 mpbird ${⊢}\left(\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\wedge {X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to {X}\mathrm{prefix}{M}\in \left(\left({M}-1\right)\mathrm{WWalksN}{G}\right)$
122 121 ex ${⊢}\left({M}\in ℕ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({X}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {X}\mathrm{prefix}{M}\in \left(\left({M}-1\right)\mathrm{WWalksN}{G}\right)\right)$