Metamath Proof Explorer

Theorem wwlksnredwwlkn

Description: For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypothesis wwlksnredwwlkn.e ⊢ E = Edg ⁡ G
Assertion wwlksnredwwlkn ⊢ N ∈ ℕ 0 → W ∈ N + 1 WWalksN G → ∃ y ∈ N WWalksN G W prefix N + 1 = y ∧ lastS ⁡ y lastS ⁡ W ∈ E

Proof

Step Hyp Ref Expression
1 wwlksnredwwlkn.e ⊢ E = Edg ⁡ G
2 eqidd ⊢ N ∈ ℕ 0 ∧ W ∈ N + 1 WWalksN G → W prefix N + 1 = W prefix N + 1
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 1 wwlknp ⊢ W ∈ N + 1 WWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E
5 simprl ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → W ∈ Word Vtx ⁡ G
6 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
7 peano2nn0 ⊢ N + 1 ∈ ℕ 0 → N + 1 + 1 ∈ ℕ 0
8 6 7 syl ⊢ N ∈ ℕ 0 → N + 1 + 1 ∈ ℕ 0
9 id ⊢ N ∈ ℕ 0 → N ∈ ℕ 0
10 nn0p1nn ⊢ N + 1 ∈ ℕ 0 → N + 1 + 1 ∈ ℕ
11 6 10 syl ⊢ N ∈ ℕ 0 → N + 1 + 1 ∈ ℕ
12 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
13 id ⊢ N ∈ ℝ → N ∈ ℝ
14 peano2re ⊢ N ∈ ℝ → N + 1 ∈ ℝ
15 peano2re ⊢ N + 1 ∈ ℝ → N + 1 + 1 ∈ ℝ
16 14 15 syl ⊢ N ∈ ℝ → N + 1 + 1 ∈ ℝ
17 13 14 16 3jca ⊢ N ∈ ℝ → N ∈ ℝ ∧ N + 1 ∈ ℝ ∧ N + 1 + 1 ∈ ℝ
18 12 17 syl ⊢ N ∈ ℕ 0 → N ∈ ℝ ∧ N + 1 ∈ ℝ ∧ N + 1 + 1 ∈ ℝ
19 12 ltp1d ⊢ N ∈ ℕ 0 → N < N + 1
20 nn0re ⊢ N + 1 ∈ ℕ 0 → N + 1 ∈ ℝ
21 6 20 syl ⊢ N ∈ ℕ 0 → N + 1 ∈ ℝ
22 21 ltp1d ⊢ N ∈ ℕ 0 → N + 1 < N + 1 + 1
23 lttr ⊢ N ∈ ℝ ∧ N + 1 ∈ ℝ ∧ N + 1 + 1 ∈ ℝ → N < N + 1 ∧ N + 1 < N + 1 + 1 → N < N + 1 + 1
24 23 imp ⊢ N ∈ ℝ ∧ N + 1 ∈ ℝ ∧ N + 1 + 1 ∈ ℝ ∧ N < N + 1 ∧ N + 1 < N + 1 + 1 → N < N + 1 + 1
25 18 19 22 24 syl12anc ⊢ N ∈ ℕ 0 → N < N + 1 + 1
26 elfzo0 ⊢ N ∈ 0 ..^ N + 1 + 1 ↔ N ∈ ℕ 0 ∧ N + 1 + 1 ∈ ℕ ∧ N < N + 1 + 1
27 9 11 25 26 syl3anbrc ⊢ N ∈ ℕ 0 → N ∈ 0 ..^ N + 1 + 1
28 fz0add1fz1 ⊢ N + 1 + 1 ∈ ℕ 0 ∧ N ∈ 0 ..^ N + 1 + 1 → N + 1 ∈ 1 … N + 1 + 1
29 8 27 28 syl2anc ⊢ N ∈ ℕ 0 → N + 1 ∈ 1 … N + 1 + 1
30 29 adantr ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N + 1 ∈ 1 … N + 1 + 1
31 oveq2 ⊢ W = N + 1 + 1 → 1 … W = 1 … N + 1 + 1
32 31 eleq2d ⊢ W = N + 1 + 1 → N + 1 ∈ 1 … W ↔ N + 1 ∈ 1 … N + 1 + 1
33 32 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N + 1 ∈ 1 … W ↔ N + 1 ∈ 1 … N + 1 + 1
34 33 adantl ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N + 1 ∈ 1 … W ↔ N + 1 ∈ 1 … N + 1 + 1
35 30 34 mpbird ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N + 1 ∈ 1 … W
36 5 35 jca ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
37 36 3adantr3 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W
38 pfxfvlsw ⊢ W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W → lastS ⁡ W prefix N + 1 = W ⁡ N + 1 - 1
39 37 38 syl ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W prefix N + 1 = W ⁡ N + 1 - 1
40 lsw ⊢ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ W − 1
41 40 3ad2ant1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W = W ⁡ W − 1
42 41 adantl ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W = W ⁡ W − 1
43 39 42 preq12d ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W prefix N + 1 lastS ⁡ W = W ⁡ N + 1 - 1 W ⁡ W − 1
44 oveq1 ⊢ W = N + 1 + 1 → W − 1 = N + 1 + 1 - 1
45 44 3ad2ant2 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W − 1 = N + 1 + 1 - 1
46 45 adantl ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W − 1 = N + 1 + 1 - 1
47 46 fveq2d ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ W − 1 = W ⁡ N + 1 + 1 - 1
48 47 preq2d ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N + 1 - 1 W ⁡ W − 1 = W ⁡ N + 1 - 1 W ⁡ N + 1 + 1 - 1
49 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
50 1cnd ⊢ N ∈ ℕ 0 → 1 ∈ ℂ
51 49 50 pncand ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
52 51 fveq2d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 - 1 = W ⁡ N
53 6 nn0cnd ⊢ N ∈ ℕ 0 → N + 1 ∈ ℂ
54 53 50 pncand ⊢ N ∈ ℕ 0 → N + 1 + 1 - 1 = N + 1
55 54 fveq2d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 + 1 - 1 = W ⁡ N + 1
56 52 55 preq12d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 - 1 W ⁡ N + 1 + 1 - 1 = W ⁡ N W ⁡ N + 1
57 56 adantr ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N + 1 - 1 W ⁡ N + 1 + 1 - 1 = W ⁡ N W ⁡ N + 1
58 48 57 eqtrd ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N + 1 - 1 W ⁡ W − 1 = W ⁡ N W ⁡ N + 1
59 fveq2 ⊢ i = N → W ⁡ i = W ⁡ N
60 fvoveq1 ⊢ i = N → W ⁡ i + 1 = W ⁡ N + 1
61 59 60 preq12d ⊢ i = N → W ⁡ i W ⁡ i + 1 = W ⁡ N W ⁡ N + 1
62 61 eleq1d ⊢ i = N → W ⁡ i W ⁡ i + 1 ∈ E ↔ W ⁡ N W ⁡ N + 1 ∈ E
63 62 rspcv ⊢ N ∈ 0 ..^ N + 1 → ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N W ⁡ N + 1 ∈ E
64 fzonn0p1 ⊢ N ∈ ℕ 0 → N ∈ 0 ..^ N + 1
65 63 64 syl11 ⊢ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → N ∈ ℕ 0 → W ⁡ N W ⁡ N + 1 ∈ E
66 65 3ad2ant3 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → N ∈ ℕ 0 → W ⁡ N W ⁡ N + 1 ∈ E
67 66 impcom ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N W ⁡ N + 1 ∈ E
68 58 67 eqeltrd ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N + 1 - 1 W ⁡ W − 1 ∈ E
69 43 68 eqeltrd ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
70 4 69 sylan2 ⊢ N ∈ ℕ 0 ∧ W ∈ N + 1 WWalksN G → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
71 wwlksnred ⊢ N ∈ ℕ 0 → W ∈ N + 1 WWalksN G → W prefix N + 1 ∈ N WWalksN G
72 71 imp ⊢ N ∈ ℕ 0 ∧ W ∈ N + 1 WWalksN G → W prefix N + 1 ∈ N WWalksN G
73 eqeq2 ⊢ y = W prefix N + 1 → W prefix N + 1 = y ↔ W prefix N + 1 = W prefix N + 1
74 fveq2 ⊢ y = W prefix N + 1 → lastS ⁡ y = lastS ⁡ W prefix N + 1
75 74 preq1d ⊢ y = W prefix N + 1 → lastS ⁡ y lastS ⁡ W = lastS ⁡ W prefix N + 1 lastS ⁡ W
76 75 eleq1d ⊢ y = W prefix N + 1 → lastS ⁡ y lastS ⁡ W ∈ E ↔ lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
77 73 76 anbi12d ⊢ y = W prefix N + 1 → W prefix N + 1 = y ∧ lastS ⁡ y lastS ⁡ W ∈ E ↔ W prefix N + 1 = W prefix N + 1 ∧ lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
78 77 adantl ⊢ N ∈ ℕ 0 ∧ W ∈ N + 1 WWalksN G ∧ y = W prefix N + 1 → W prefix N + 1 = y ∧ lastS ⁡ y lastS ⁡ W ∈ E ↔ W prefix N + 1 = W prefix N + 1 ∧ lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
79 72 78 rspcedv ⊢ N ∈ ℕ 0 ∧ W ∈ N + 1 WWalksN G → W prefix N + 1 = W prefix N + 1 ∧ lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E → ∃ y ∈ N WWalksN G W prefix N + 1 = y ∧ lastS ⁡ y lastS ⁡ W ∈ E
80 2 70 79 mp2and ⊢ N ∈ ℕ 0 ∧ W ∈ N + 1 WWalksN G → ∃ y ∈ N WWalksN G W prefix N + 1 = y ∧ lastS ⁡ y lastS ⁡ W ∈ E
81 80 ex ⊢ N ∈ ℕ 0 → W ∈ N + 1 WWalksN G → ∃ y ∈ N WWalksN G W prefix N + 1 = y ∧ lastS ⁡ y lastS ⁡ W ∈ E