Metamath Proof Explorer

Theorem wwlksnred

Description: Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Assertion wwlksnred ⊢N∈ℕ0→W∈N+1WWalksNG→WprefixN+1∈NWWalksNG

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢N∈ℕ0→N+1∈ℕ0
2 iswwlksn ⊢N+1∈ℕ0→W∈N+1WWalksNG↔W∈WWalks⁡G∧W=N+1+1
3 1 2 syl ⊢N∈ℕ0→W∈N+1WWalksNG↔W∈WWalks⁡G∧W=N+1+1
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 eqid ⊢Edg⁡G=Edg⁡G
6 4 5 iswwlks ⊢W∈WWalks⁡G↔W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G
7 simp1 ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G
8 nn0p1nn ⊢N∈ℕ0→N+1∈ℕ
9 8 3ad2ant3 ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈ℕ
10 1 nn0red ⊢N∈ℕ0→N+1∈ℝ
11 10 lep1d ⊢N∈ℕ0→N+1≤N+1+1
12 11 3ad2ant3 ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1≤N+1+1
13 breq2 ⊢W=N+1+1→N+1≤W↔N+1≤N+1+1
14 13 3ad2ant2 ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1≤W↔N+1≤N+1+1
15 12 14 mpbird ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1≤W
16 pfxn0 ⊢W∈WordVtx⁡G∧N+1∈ℕ∧N+1≤W→WprefixN+1≠∅
17 7 9 15 16 syl3anc ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→WprefixN+1≠∅
18 17 3exp ⊢W∈WordVtx⁡G→W=N+1+1→N∈ℕ0→WprefixN+1≠∅
19 18 3ad2ant2 ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→W=N+1+1→N∈ℕ0→WprefixN+1≠∅
20 19 imp ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→N∈ℕ0→WprefixN+1≠∅
21 20 impcom ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1≠∅
22 pfxcl ⊢W∈WordVtx⁡G→WprefixN+1∈WordVtx⁡G
23 22 3ad2ant2 ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→WprefixN+1∈WordVtx⁡G
24 23 adantr ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1∈WordVtx⁡G
25 24 adantl ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1∈WordVtx⁡G
26 oveq1 ⊢W=N+1+1→W−1=N+1+1-1
27 1 nn0cnd ⊢N∈ℕ0→N+1∈ℂ
28 1cnd ⊢N∈ℕ0→1∈ℂ
29 27 28 pncand ⊢N∈ℕ0→N+1+1-1=N+1
30 26 29 sylan9eq ⊢W=N+1+1∧N∈ℕ0→W−1=N+1
31 30 oveq2d ⊢W=N+1+1∧N∈ℕ0→0..^W−1=0..^N+1
32 31 raleqdv ⊢W=N+1+1∧N∈ℕ0→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G↔∀i∈0..^N+1W⁡iW⁡i+1∈Edg⁡G
33 32 adantl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G↔∀i∈0..^N+1W⁡iW⁡i+1∈Edg⁡G
34 nn0z ⊢N∈ℕ0→N∈ℤ
35 nn0z ⊢N+1∈ℕ0→N+1∈ℤ
36 1 35 syl ⊢N∈ℕ0→N+1∈ℤ
37 nn0re ⊢N∈ℕ0→N∈ℝ
38 37 lep1d ⊢N∈ℕ0→N≤N+1
39 34 36 38 3jca ⊢N∈ℕ0→N∈ℤ∧N+1∈ℤ∧N≤N+1
40 39 ad2antll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N∈ℤ∧N+1∈ℤ∧N≤N+1
41 eluz2 ⊢N+1∈ℤ≥N↔N∈ℤ∧N+1∈ℤ∧N≤N+1
42 40 41 sylibr ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈ℤ≥N
43 fzoss2 ⊢N+1∈ℤ≥N→0..^N⊆0..^N+1
44 42 43 syl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→0..^N⊆0..^N+1
45 ssralv ⊢0..^N⊆0..^N+1→∀i∈0..^N+1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G
46 44 45 syl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^N+1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G
47 simpll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→W∈WordVtx⁡G
48 nn0fz0 ⊢N+1∈ℕ0↔N+1∈0…N+1
49 1 48 sylib ⊢N∈ℕ0→N+1∈0…N+1
50 49 ad2antll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈0…N+1
51 fzelp1 ⊢N+1∈0…N+1→N+1∈0…N+1+1
52 50 51 syl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈0…N+1+1
53 oveq2 ⊢W=N+1+1→0…W=0…N+1+1
54 53 eleq2d ⊢W=N+1+1→N+1∈0…W↔N+1∈0…N+1+1
55 54 adantr ⊢W=N+1+1∧N∈ℕ0→N+1∈0…W↔N+1∈0…N+1+1
56 55 adantl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈0…W↔N+1∈0…N+1+1
57 52 56 mpbird ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈0…W
58 57 adantr ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→N+1∈0…W
59 fzossfzop1 ⊢N∈ℕ0→0..^N⊆0..^N+1
60 59 sseld ⊢N∈ℕ0→i∈0..^N→i∈0..^N+1
61 60 ad2antll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→i∈0..^N→i∈0..^N+1
62 61 imp ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→i∈0..^N+1
63 pfxfv ⊢W∈WordVtx⁡G∧N+1∈0…W∧i∈0..^N+1→WprefixN+1⁡i=W⁡i
64 47 58 62 63 syl3anc ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→WprefixN+1⁡i=W⁡i
65 64 eqcomd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→W⁡i=WprefixN+1⁡i
66 fzofzp1 ⊢i∈0..^N→i+1∈0…N
67 66 adantl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→i+1∈0…N
68 fzval3 ⊢N∈ℤ→0…N=0..^N+1
69 68 eqcomd ⊢N∈ℤ→0..^N+1=0…N
70 34 69 syl ⊢N∈ℕ0→0..^N+1=0…N
71 70 eleq2d ⊢N∈ℕ0→i+1∈0..^N+1↔i+1∈0…N
72 71 ad2antll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→i+1∈0..^N+1↔i+1∈0…N
73 72 adantr ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→i+1∈0..^N+1↔i+1∈0…N
74 67 73 mpbird ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→i+1∈0..^N+1
75 pfxfv ⊢W∈WordVtx⁡G∧N+1∈0…W∧i+1∈0..^N+1→WprefixN+1⁡i+1=W⁡i+1
76 47 58 74 75 syl3anc ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→WprefixN+1⁡i+1=W⁡i+1
77 76 eqcomd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→W⁡i+1=WprefixN+1⁡i+1
78 65 77 preq12d ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→W⁡iW⁡i+1=WprefixN+1⁡iWprefixN+1⁡i+1
79 78 eleq1d ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→W⁡iW⁡i+1∈Edg⁡G↔WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
80 79 biimpd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧i∈0..^N→W⁡iW⁡i+1∈Edg⁡G→WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
81 80 ralimdva ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→∀i∈0..^NWprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
82 46 81 syld ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^N+1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^NWprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
83 33 82 sylbid ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^NWprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
84 83 imp ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^NWprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
85 nn0cn ⊢N∈ℕ0→N∈ℂ
86 85 28 pncand ⊢N∈ℕ0→N+1-1=N
87 86 oveq2d ⊢N∈ℕ0→0..^N+1-1=0..^N
88 87 ad2antll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→0..^N+1-1=0..^N
89 88 adantr ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→0..^N+1-1=0..^N
90 89 raleqdv ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^N+1-1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G↔∀i∈0..^NWprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
91 84 90 mpbird ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^N+1-1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
92 pfxlen ⊢W∈WordVtx⁡G∧N+1∈0…W→WprefixN+1=N+1
93 57 92 syldan ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→WprefixN+1=N+1
94 93 oveq1d ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→WprefixN+1−1=N+1-1
95 94 oveq2d ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→0..^WprefixN+1−1=0..^N+1-1
96 95 raleqdv ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G↔∀i∈0..^N+1-1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
97 96 adantr ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G↔∀i∈0..^N+1-1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
98 91 97 mpbird ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
99 98 exp31 ⊢W∈WordVtx⁡G→W=N+1+1∧N∈ℕ0→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
100 99 com23 ⊢W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→W=N+1+1∧N∈ℕ0→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
101 100 imp ⊢W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→W=N+1+1∧N∈ℕ0→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
102 101 3adant1 ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→W=N+1+1∧N∈ℕ0→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
103 102 expdimp ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→N∈ℕ0→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
104 103 impcom ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
105 4 5 iswwlks ⊢WprefixN+1∈WWalks⁡G↔WprefixN+1≠∅∧WprefixN+1∈WordVtx⁡G∧∀i∈0..^WprefixN+1−1WprefixN+1⁡iWprefixN+1⁡i+1∈Edg⁡G
106 21 25 104 105 syl3anbrc ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1∈WWalks⁡G
107 peano2nn0 ⊢N+1∈ℕ0→N+1+1∈ℕ0
108 1 107 syl ⊢N∈ℕ0→N+1+1∈ℕ0
109 elfz2nn0 ⊢N+1∈0…N+1+1↔N+1∈ℕ0∧N+1+1∈ℕ0∧N+1≤N+1+1
110 1 108 11 109 syl3anbrc ⊢N∈ℕ0→N+1∈0…N+1+1
111 110 adantl ⊢W=N+1+1∧N∈ℕ0→N+1∈0…N+1+1
112 111 55 mpbird ⊢W=N+1+1∧N∈ℕ0→N+1∈0…W
113 112 anim2i ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
114 113 exp32 ⊢W∈WordVtx⁡G→W=N+1+1→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
115 114 3ad2ant2 ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G→W=N+1+1→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
116 115 imp ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
117 116 impcom ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→W∈WordVtx⁡G∧N+1∈0…W
118 117 92 syl ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1=N+1
119 iswwlksn ⊢N∈ℕ0→WprefixN+1∈NWWalksNG↔WprefixN+1∈WWalks⁡G∧WprefixN+1=N+1
120 119 adantr ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1∈NWWalksNG↔WprefixN+1∈WWalks⁡G∧WprefixN+1=N+1
121 106 118 120 mpbir2and ⊢N∈ℕ0∧W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→WprefixN+1∈NWWalksNG
122 121 expcom ⊢W≠∅∧W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧W=N+1+1→N∈ℕ0→WprefixN+1∈NWWalksNG
123 6 122 sylanb ⊢W∈WWalks⁡G∧W=N+1+1→N∈ℕ0→WprefixN+1∈NWWalksNG
124 123 com12 ⊢N∈ℕ0→W∈WWalks⁡G∧W=N+1+1→WprefixN+1∈NWWalksNG
125 3 124 sylbid ⊢N∈ℕ0→W∈N+1WWalksNG→WprefixN+1∈NWWalksNG