Metamath Proof Explorer

Theorem wwlksm1edg

Description: Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Assertion wwlksm1edg ⊢W∈WWalks⁡G∧2≤W→WprefixW−1∈WWalks⁡G

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢Edg⁡G=Edg⁡G
3 1 2 iswwlks ⊢W∈WWalks⁡G↔W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G
4 lencl ⊢W∈WordVtx⁡G→W∈ℕ0
5 simpl ⊢W∈ℕ0∧2≤W→W∈ℕ0
6 1red ⊢W∈ℕ0∧2≤W→1∈ℝ
7 2re ⊢2∈ℝ
8 7 a1i ⊢W∈ℕ0∧2≤W→2∈ℝ
9 nn0re ⊢W∈ℕ0→W∈ℝ
10 9 adantr ⊢W∈ℕ0∧2≤W→W∈ℝ
11 1le2 ⊢1≤2
12 11 a1i ⊢W∈ℕ0∧2≤W→1≤2
13 simpr ⊢W∈ℕ0∧2≤W→2≤W
14 6 8 10 12 13 letrd ⊢W∈ℕ0∧2≤W→1≤W
15 5 14 jca ⊢W∈ℕ0∧2≤W→W∈ℕ0∧1≤W
16 elnnnn0c ⊢W∈ℕ↔W∈ℕ0∧1≤W
17 15 16 sylibr ⊢W∈ℕ0∧2≤W→W∈ℕ
18 lbfzo0 ⊢0∈0..^W↔W∈ℕ
19 17 18 sylibr ⊢W∈ℕ0∧2≤W→0∈0..^W
20 nn0ge2m1nn ⊢W∈ℕ0∧2≤W→W−1∈ℕ
21 lbfzo0 ⊢0∈0..^W−1↔W−1∈ℕ
22 20 21 sylibr ⊢W∈ℕ0∧2≤W→0∈0..^W−1
23 19 22 jca ⊢W∈ℕ0∧2≤W→0∈0..^W∧0∈0..^W−1
24 4 23 sylan ⊢W∈WordVtx⁡G∧2≤W→0∈0..^W∧0∈0..^W−1
25 inelcm ⊢0∈0..^W∧0∈0..^W−1→0..^W∩0..^W−1≠∅
26 24 25 syl ⊢W∈WordVtx⁡G∧2≤W→0..^W∩0..^W−1≠∅
27 wrdfn ⊢W∈WordVtx⁡G→WFn0..^W
28 27 adantr ⊢W∈WordVtx⁡G∧2≤W→WFn0..^W
29 fnresdisj ⊢WFn0..^W→0..^W∩0..^W−1=∅↔W↾0..^W−1=∅
30 28 29 syl ⊢W∈WordVtx⁡G∧2≤W→0..^W∩0..^W−1=∅↔W↾0..^W−1=∅
31 nn0ge2m1nn0 ⊢W∈ℕ0∧2≤W→W−1∈ℕ0
32 10 lem1d ⊢W∈ℕ0∧2≤W→W−1≤W
33 31 5 32 3jca ⊢W∈ℕ0∧2≤W→W−1∈ℕ0∧W∈ℕ0∧W−1≤W
34 4 33 sylan ⊢W∈WordVtx⁡G∧2≤W→W−1∈ℕ0∧W∈ℕ0∧W−1≤W
35 elfz2nn0 ⊢W−1∈0…W↔W−1∈ℕ0∧W∈ℕ0∧W−1≤W
36 34 35 sylibr ⊢W∈WordVtx⁡G∧2≤W→W−1∈0…W
37 pfxres ⊢W∈WordVtx⁡G∧W−1∈0…W→WprefixW−1=W↾0..^W−1
38 37 eqeq1d ⊢W∈WordVtx⁡G∧W−1∈0…W→WprefixW−1=∅↔W↾0..^W−1=∅
39 38 bicomd ⊢W∈WordVtx⁡G∧W−1∈0…W→W↾0..^W−1=∅↔WprefixW−1=∅
40 36 39 syldan ⊢W∈WordVtx⁡G∧2≤W→W↾0..^W−1=∅↔WprefixW−1=∅
41 30 40 bitr2d ⊢W∈WordVtx⁡G∧2≤W→WprefixW−1=∅↔0..^W∩0..^W−1=∅
42 41 necon3bid ⊢W∈WordVtx⁡G∧2≤W→WprefixW−1≠∅↔0..^W∩0..^W−1≠∅
43 26 42 mpbird ⊢W∈WordVtx⁡G∧2≤W→WprefixW−1≠∅
44 43 3ad2antl2 ⊢W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G∧2≤W→WprefixW−1≠∅
45 pfxcl ⊢W∈WordVtx⁡G→WprefixW−1∈WordVtx⁡G
46 45 a1d ⊢W∈WordVtx⁡G→2≤W→WprefixW−1∈WordVtx⁡G
47 46 3ad2ant2 ⊢W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→2≤W→WprefixW−1∈WordVtx⁡G
48 47 imp ⊢W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G∧2≤W→WprefixW−1∈WordVtx⁡G
49 nn0z ⊢W∈ℕ0→W∈ℤ
50 peano2zm ⊢W∈ℤ→W−1∈ℤ
51 49 50 syl ⊢W∈ℕ0→W−1∈ℤ
52 peano2zm ⊢W−1∈ℤ→W-1-1∈ℤ
53 51 52 syl ⊢W∈ℕ0→W-1-1∈ℤ
54 53 adantr ⊢W∈ℕ0∧2≤W→W-1-1∈ℤ
55 51 adantr ⊢W∈ℕ0∧2≤W→W−1∈ℤ
56 peano2rem ⊢W∈ℝ→W−1∈ℝ
57 9 56 syl ⊢W∈ℕ0→W−1∈ℝ
58 57 lem1d ⊢W∈ℕ0→W-1-1≤W−1
59 58 adantr ⊢W∈ℕ0∧2≤W→W-1-1≤W−1
60 54 55 59 3jca ⊢W∈ℕ0∧2≤W→W-1-1∈ℤ∧W−1∈ℤ∧W-1-1≤W−1
61 4 60 sylan ⊢W∈WordVtx⁡G∧2≤W→W-1-1∈ℤ∧W−1∈ℤ∧W-1-1≤W−1
62 eluz2 ⊢W−1∈ℤ≥W-1-1↔W-1-1∈ℤ∧W−1∈ℤ∧W-1-1≤W−1
63 61 62 sylibr ⊢W∈WordVtx⁡G∧2≤W→W−1∈ℤ≥W-1-1
64 9 lem1d ⊢W∈ℕ0→W−1≤W
65 64 adantr ⊢W∈ℕ0∧2≤W→W−1≤W
66 31 5 65 3jca ⊢W∈ℕ0∧2≤W→W−1∈ℕ0∧W∈ℕ0∧W−1≤W
67 4 66 sylan ⊢W∈WordVtx⁡G∧2≤W→W−1∈ℕ0∧W∈ℕ0∧W−1≤W
68 67 35 sylibr ⊢W∈WordVtx⁡G∧2≤W→W−1∈0…W
69 pfxlen ⊢W∈WordVtx⁡G∧W−1∈0…W→WprefixW−1=W−1
70 69 oveq1d ⊢W∈WordVtx⁡G∧W−1∈0…W→WprefixW−1−1=W-1-1
71 68 70 syldan ⊢W∈WordVtx⁡G∧2≤W→WprefixW−1−1=W-1-1
72 71 fveq2d ⊢W∈WordVtx⁡G∧2≤W→ℤ≥WprefixW−1−1=ℤ≥W-1-1
73 63 72 eleqtrrd ⊢W∈WordVtx⁡G∧2≤W→W−1∈ℤ≥WprefixW−1−1
74 fzoss2 ⊢W−1∈ℤ≥WprefixW−1−1→0..^WprefixW−1−1⊆0..^W−1
75 73 74 syl ⊢W∈WordVtx⁡G∧2≤W→0..^WprefixW−1−1⊆0..^W−1
76 ssralv ⊢0..^WprefixW−1−1⊆0..^W−1→∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→∀x∈0..^WprefixW−1−1W⁡xW⁡x+1∈Edg⁡G
77 75 76 syl ⊢W∈WordVtx⁡G∧2≤W→∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→∀x∈0..^WprefixW−1−1W⁡xW⁡x+1∈Edg⁡G
78 68 69 syldan ⊢W∈WordVtx⁡G∧2≤W→WprefixW−1=W−1
79 78 oveq1d ⊢W∈WordVtx⁡G∧2≤W→WprefixW−1−1=W-1-1
80 79 oveq2d ⊢W∈WordVtx⁡G∧2≤W→0..^WprefixW−1−1=0..^W-1-1
81 80 eleq2d ⊢W∈WordVtx⁡G∧2≤W→x∈0..^WprefixW−1−1↔x∈0..^W-1-1
82 simpl ⊢W∈WordVtx⁡G∧2≤W→W∈WordVtx⁡G
83 82 adantr ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→W∈WordVtx⁡G
84 36 adantr ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→W−1∈0…W
85 4 31 sylan ⊢W∈WordVtx⁡G∧2≤W→W−1∈ℕ0
86 nn0z ⊢W−1∈ℕ0→W−1∈ℤ
87 fzossrbm1 ⊢W−1∈ℤ→0..^W-1-1⊆0..^W−1
88 86 87 syl ⊢W−1∈ℕ0→0..^W-1-1⊆0..^W−1
89 85 88 syl ⊢W∈WordVtx⁡G∧2≤W→0..^W-1-1⊆0..^W−1
90 89 sselda ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→x∈0..^W−1
91 pfxfv ⊢W∈WordVtx⁡G∧W−1∈0…W∧x∈0..^W−1→WprefixW−1⁡x=W⁡x
92 83 84 90 91 syl3anc ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→WprefixW−1⁡x=W⁡x
93 92 eqcomd ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→W⁡x=WprefixW−1⁡x
94 4 20 sylan ⊢W∈WordVtx⁡G∧2≤W→W−1∈ℕ
95 elfzom1p1elfzo ⊢W−1∈ℕ∧x∈0..^W-1-1→x+1∈0..^W−1
96 94 95 sylan ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→x+1∈0..^W−1
97 pfxfv ⊢W∈WordVtx⁡G∧W−1∈0…W∧x+1∈0..^W−1→WprefixW−1⁡x+1=W⁡x+1
98 83 84 96 97 syl3anc ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→WprefixW−1⁡x+1=W⁡x+1
99 98 eqcomd ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→W⁡x+1=WprefixW−1⁡x+1
100 93 99 preq12d ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^W-1-1→W⁡xW⁡x+1=WprefixW−1⁡xWprefixW−1⁡x+1
101 100 ex ⊢W∈WordVtx⁡G∧2≤W→x∈0..^W-1-1→W⁡xW⁡x+1=WprefixW−1⁡xWprefixW−1⁡x+1
102 81 101 sylbid ⊢W∈WordVtx⁡G∧2≤W→x∈0..^WprefixW−1−1→W⁡xW⁡x+1=WprefixW−1⁡xWprefixW−1⁡x+1
103 102 imp ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^WprefixW−1−1→W⁡xW⁡x+1=WprefixW−1⁡xWprefixW−1⁡x+1
104 103 eleq1d ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^WprefixW−1−1→W⁡xW⁡x+1∈Edg⁡G↔WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
105 104 biimpd ⊢W∈WordVtx⁡G∧2≤W∧x∈0..^WprefixW−1−1→W⁡xW⁡x+1∈Edg⁡G→WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
106 105 ralimdva ⊢W∈WordVtx⁡G∧2≤W→∀x∈0..^WprefixW−1−1W⁡xW⁡x+1∈Edg⁡G→∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
107 77 106 syld ⊢W∈WordVtx⁡G∧2≤W→∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
108 107 expcom ⊢2≤W→W∈WordVtx⁡G→∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
109 108 com3l ⊢W∈WordVtx⁡G→∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→2≤W→∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
110 109 a1i ⊢W≠∅→W∈WordVtx⁡G→∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→2≤W→∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
111 110 3imp1 ⊢W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G∧2≤W→∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
112 1 2 iswwlks ⊢WprefixW−1∈WWalks⁡G↔WprefixW−1≠∅∧WprefixW−1∈WordVtx⁡G∧∀x∈0..^WprefixW−1−1WprefixW−1⁡xWprefixW−1⁡x+1∈Edg⁡G
113 44 48 111 112 syl3anbrc ⊢W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G∧2≤W→WprefixW−1∈WWalks⁡G
114 113 ex ⊢W≠∅∧W∈WordVtx⁡G∧∀x∈0..^W−1W⁡xW⁡x+1∈Edg⁡G→2≤W→WprefixW−1∈WWalks⁡G
115 3 114 sylbi ⊢W∈WWalks⁡G→2≤W→WprefixW−1∈WWalks⁡G
116 115 imp ⊢W∈WWalks⁡G∧2≤W→WprefixW−1∈WWalks⁡G