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 → W prefix W − 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 ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G
4 lencl ⊢ W ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ 2 ≤ W → 0 ..^ W ∩ 0 ..^ W − 1 ≠ ∅
27 wrdfn ⊢ W ∈ Word Vtx ⁡ G → W Fn 0 ..^ W
28 27 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W Fn 0 ..^ W
29 fnresdisj ⊢ W Fn 0 ..^ W → 0 ..^ W ∩ 0 ..^ W − 1 = ∅ ↔ W ↾ 0 ..^ W − 1 = ∅
30 28 29 syl ⊢ W ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W − 1 ∈ 0 … W
37 pfxres ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W → W prefix W − 1 = W ↾ 0 ..^ W − 1
38 37 eqeq1d ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W → W prefix W − 1 = ∅ ↔ W ↾ 0 ..^ W − 1 = ∅
39 38 bicomd ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W → W ↾ 0 ..^ W − 1 = ∅ ↔ W prefix W − 1 = ∅
40 36 39 syldan ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W ↾ 0 ..^ W − 1 = ∅ ↔ W prefix W − 1 = ∅
41 30 40 bitr2d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W prefix W − 1 = ∅ ↔ 0 ..^ W ∩ 0 ..^ W − 1 = ∅
42 41 necon3bid ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W prefix W − 1 ≠ ∅ ↔ 0 ..^ W ∩ 0 ..^ W − 1 ≠ ∅
43 26 42 mpbird ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W prefix W − 1 ≠ ∅
44 43 3ad2antl2 ⊢ W ≠ ∅ ∧ W ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G ∧ 2 ≤ W → W prefix W − 1 ≠ ∅
45 pfxcl ⊢ W ∈ Word Vtx ⁡ G → W prefix W − 1 ∈ Word Vtx ⁡ G
46 45 a1d ⊢ W ∈ Word Vtx ⁡ G → 2 ≤ W → W prefix W − 1 ∈ Word Vtx ⁡ G
47 46 3ad2ant2 ⊢ W ≠ ∅ ∧ W ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → 2 ≤ W → W prefix W − 1 ∈ Word Vtx ⁡ G
48 47 imp ⊢ W ≠ ∅ ∧ W ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G ∧ 2 ≤ W → W prefix W − 1 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W − 1 ∈ ℕ 0 ∧ W ∈ ℕ 0 ∧ W − 1 ≤ W
68 67 35 sylibr ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W − 1 ∈ 0 … W
69 pfxlen ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W → W prefix W − 1 = W − 1
70 69 oveq1d ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W → W prefix W − 1 − 1 = W - 1 - 1
71 68 70 syldan ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W prefix W − 1 − 1 = W - 1 - 1
72 71 fveq2d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → ℤ ≥ W prefix W − 1 − 1 = ℤ ≥ W - 1 - 1
73 63 72 eleqtrrd ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W − 1 ∈ ℤ ≥ W prefix W − 1 − 1
74 fzoss2 ⊢ W − 1 ∈ ℤ ≥ W prefix W − 1 − 1 → 0 ..^ W prefix W − 1 − 1 ⊆ 0 ..^ W − 1
75 73 74 syl ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → 0 ..^ W prefix W − 1 − 1 ⊆ 0 ..^ W − 1
76 ssralv ⊢ 0 ..^ W prefix W − 1 − 1 ⊆ 0 ..^ W − 1 → ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G
77 75 76 syl ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G
78 68 69 syldan ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W prefix W − 1 = W − 1
79 78 oveq1d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W prefix W − 1 − 1 = W - 1 - 1
80 79 oveq2d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → 0 ..^ W prefix W − 1 − 1 = 0 ..^ W - 1 - 1
81 80 eleq2d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → x ∈ 0 ..^ W prefix W − 1 − 1 ↔ x ∈ 0 ..^ W - 1 - 1
82 simpl ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W ∈ Word Vtx ⁡ G
83 82 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W ∈ Word Vtx ⁡ G
84 36 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W − 1 ∈ 0 … W
85 4 31 sylan ⊢ W ∈ Word Vtx ⁡ 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 ∈ Word Vtx ⁡ G ∧ 2 ≤ W → 0 ..^ W - 1 - 1 ⊆ 0 ..^ W − 1
90 89 sselda ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → x ∈ 0 ..^ W − 1
91 pfxfv ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W ∧ x ∈ 0 ..^ W − 1 → W prefix W − 1 ⁡ x = W ⁡ x
92 83 84 90 91 syl3anc ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W prefix W − 1 ⁡ x = W ⁡ x
93 92 eqcomd ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W ⁡ x = W prefix W − 1 ⁡ x
94 4 20 sylan ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → W − 1 ∈ ℕ
95 elfzom1p1elfzo ⊢ W − 1 ∈ ℕ ∧ x ∈ 0 ..^ W - 1 - 1 → x + 1 ∈ 0 ..^ W − 1
96 94 95 sylan ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → x + 1 ∈ 0 ..^ W − 1
97 pfxfv ⊢ W ∈ Word Vtx ⁡ G ∧ W − 1 ∈ 0 … W ∧ x + 1 ∈ 0 ..^ W − 1 → W prefix W − 1 ⁡ x + 1 = W ⁡ x + 1
98 83 84 96 97 syl3anc ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W prefix W − 1 ⁡ x + 1 = W ⁡ x + 1
99 98 eqcomd ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W ⁡ x + 1 = W prefix W − 1 ⁡ x + 1
100 93 99 preq12d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W - 1 - 1 → W ⁡ x W ⁡ x + 1 = W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1
101 100 ex ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → x ∈ 0 ..^ W - 1 - 1 → W ⁡ x W ⁡ x + 1 = W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1
102 81 101 sylbid ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → x ∈ 0 ..^ W prefix W − 1 − 1 → W ⁡ x W ⁡ x + 1 = W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1
103 102 imp ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W prefix W − 1 − 1 → W ⁡ x W ⁡ x + 1 = W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1
104 103 eleq1d ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W prefix W − 1 − 1 → W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G ↔ W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
105 104 biimpd ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W ∧ x ∈ 0 ..^ W prefix W − 1 − 1 → W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
106 105 ralimdva ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
107 77 106 syld ⊢ W ∈ Word Vtx ⁡ G ∧ 2 ≤ W → ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
108 107 expcom ⊢ 2 ≤ W → W ∈ Word Vtx ⁡ G → ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
109 108 com3l ⊢ W ∈ Word Vtx ⁡ G → ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → 2 ≤ W → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
110 109 a1i ⊢ W ≠ ∅ → W ∈ Word Vtx ⁡ G → ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → 2 ≤ W → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
111 110 3imp1 ⊢ W ≠ ∅ ∧ W ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G ∧ 2 ≤ W → ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
112 1 2 iswwlks ⊢ W prefix W − 1 ∈ WWalks ⁡ G ↔ W prefix W − 1 ≠ ∅ ∧ W prefix W − 1 ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W prefix W − 1 − 1 W prefix W − 1 ⁡ x W prefix W − 1 ⁡ x + 1 ∈ Edg ⁡ G
113 44 48 111 112 syl3anbrc ⊢ W ≠ ∅ ∧ W ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G ∧ 2 ≤ W → W prefix W − 1 ∈ WWalks ⁡ G
114 113 ex ⊢ W ≠ ∅ ∧ W ∈ Word Vtx ⁡ G ∧ ∀ x ∈ 0 ..^ W − 1 W ⁡ x W ⁡ x + 1 ∈ Edg ⁡ G → 2 ≤ W → W prefix W − 1 ∈ WWalks ⁡ G
115 3 114 sylbi ⊢ W ∈ WWalks ⁡ G → 2 ≤ W → W prefix W − 1 ∈ WWalks ⁡ G
116 115 imp ⊢ W ∈ WWalks ⁡ G ∧ 2 ≤ W → W prefix W − 1 ∈ WWalks ⁡ G