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+1WWalksNG→∃y∈NWWalksNGWprefixN+1=y∧lastS⁡ylastS⁡W∈E

Proof

Step Hyp Ref Expression
1 wwlksnredwwlkn.e ⊢E=Edg⁡G
2 eqidd ⊢N∈ℕ0∧W∈N+1WWalksNG→WprefixN+1=WprefixN+1
3 eqid ⊢Vtx⁡G=Vtx⁡G
4 3 1 wwlknp ⊢W∈N+1WWalksNG→W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E
5 simprl ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→W∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡G∧W=N+1+1→N+1∈1…W↔N+1∈1…N+1+1
34 33 adantl ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N+1∈1…W↔N+1∈1…N+1+1
35 30 34 mpbird ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→N+1∈1…W
36 5 35 jca ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1→W∈WordVtx⁡G∧N+1∈1…W
37 36 3adantr3 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W∈WordVtx⁡G∧N+1∈1…W
38 pfxfvlsw ⊢W∈WordVtx⁡G∧N+1∈1…W→lastS⁡WprefixN+1=W⁡N+1-1
39 37 38 syl ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡WprefixN+1=W⁡N+1-1
40 lsw ⊢W∈WordVtx⁡G→lastS⁡W=W⁡W−1
41 40 3ad2ant1 ⊢W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡W=W⁡W−1
42 41 adantl ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡W=W⁡W−1
43 39 42 preq12d ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡WprefixN+1lastS⁡W=W⁡N+1-1W⁡W−1
44 oveq1 ⊢W=N+1+1→W−1=N+1+1-1
45 44 3ad2ant2 ⊢W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W−1=N+1+1-1
46 45 adantl ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W−1=N+1+1-1
47 46 fveq2d ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡W−1=W⁡N+1+1-1
48 47 preq2d ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡N+1-1W⁡W−1=W⁡N+1-1W⁡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-1W⁡N+1+1-1=W⁡NW⁡N+1
57 56 adantr ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡N+1-1W⁡N+1+1-1=W⁡NW⁡N+1
58 48 57 eqtrd ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡N+1-1W⁡W−1=W⁡NW⁡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⁡iW⁡i+1=W⁡NW⁡N+1
62 61 eleq1d ⊢i=N→W⁡iW⁡i+1∈E↔W⁡NW⁡N+1∈E
63 62 rspcv ⊢N∈0..^N+1→∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡NW⁡N+1∈E
64 fzonn0p1 ⊢N∈ℕ0→N∈0..^N+1
65 63 64 syl11 ⊢∀i∈0..^N+1W⁡iW⁡i+1∈E→N∈ℕ0→W⁡NW⁡N+1∈E
66 65 3ad2ant3 ⊢W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→N∈ℕ0→W⁡NW⁡N+1∈E
67 66 impcom ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡NW⁡N+1∈E
68 58 67 eqeltrd ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡N+1-1W⁡W−1∈E
69 43 68 eqeltrd ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡WprefixN+1lastS⁡W∈E
70 4 69 sylan2 ⊢N∈ℕ0∧W∈N+1WWalksNG→lastS⁡WprefixN+1lastS⁡W∈E
71 wwlksnred ⊢N∈ℕ0→W∈N+1WWalksNG→WprefixN+1∈NWWalksNG
72 71 imp ⊢N∈ℕ0∧W∈N+1WWalksNG→WprefixN+1∈NWWalksNG
73 eqeq2 ⊢y=WprefixN+1→WprefixN+1=y↔WprefixN+1=WprefixN+1
74 fveq2 ⊢y=WprefixN+1→lastS⁡y=lastS⁡WprefixN+1
75 74 preq1d ⊢y=WprefixN+1→lastS⁡ylastS⁡W=lastS⁡WprefixN+1lastS⁡W
76 75 eleq1d ⊢y=WprefixN+1→lastS⁡ylastS⁡W∈E↔lastS⁡WprefixN+1lastS⁡W∈E
77 73 76 anbi12d ⊢y=WprefixN+1→WprefixN+1=y∧lastS⁡ylastS⁡W∈E↔WprefixN+1=WprefixN+1∧lastS⁡WprefixN+1lastS⁡W∈E
78 77 adantl ⊢N∈ℕ0∧W∈N+1WWalksNG∧y=WprefixN+1→WprefixN+1=y∧lastS⁡ylastS⁡W∈E↔WprefixN+1=WprefixN+1∧lastS⁡WprefixN+1lastS⁡W∈E
79 72 78 rspcedv ⊢N∈ℕ0∧W∈N+1WWalksNG→WprefixN+1=WprefixN+1∧lastS⁡WprefixN+1lastS⁡W∈E→∃y∈NWWalksNGWprefixN+1=y∧lastS⁡ylastS⁡W∈E
80 2 70 79 mp2and ⊢N∈ℕ0∧W∈N+1WWalksNG→∃y∈NWWalksNGWprefixN+1=y∧lastS⁡ylastS⁡W∈E
81 80 ex ⊢N∈ℕ0→W∈N+1WWalksNG→∃y∈NWWalksNGWprefixN+1=y∧lastS⁡ylastS⁡W∈E