Metamath Proof Explorer

Theorem wwlksnextproplem2

Description: Lemma 2 for wwlksnextprop . (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlksnextproplem2 ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
2 wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 2 wwlknp ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
5 fzonn0p1 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
6 5 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
7 fveq2 ⊢ ( 𝑖 = 𝑁 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑁 ) )
8 fvoveq1 ⊢ ( 𝑖 = 𝑁 → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
9 7 8 preq12d ⊢ ( 𝑖 = 𝑁 → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
10 9 eleq1d ⊢ ( 𝑖 = 𝑁 → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
11 10 rspcv ⊢ ( 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
12 6 11 syl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
13 12 imp ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 )
14 simpll ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
15 1zzd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℤ )
16 lencl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
17 16 nn0zd ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
18 17 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
19 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
20 19 nn0zd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
21 20 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℤ )
22 15 18 21 3jca ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) )
23 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
24 1red ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
25 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
26 24 25 addge02d ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ≤ 𝑁 ↔ 1 ≤ ( 𝑁 + 1 ) ) )
27 23 26 mpbid ⊢ ( 𝑁 ∈ ℕ0 → 1 ≤ ( 𝑁 + 1 ) )
28 27 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ ( 𝑁 + 1 ) )
29 19 nn0red ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
30 29 lep1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
31 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
32 30 31 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
33 32 a1i ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
34 33 com23 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
35 16 34 syl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
36 35 imp31 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) )
37 28 36 jca ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 1 ≤ ( 𝑁 + 1 ) ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
38 elfz2 ⊢ ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) ∧ ( 1 ≤ ( 𝑁 + 1 ) ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
39 22 37 38 sylanbrc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
40 pfxfvlsw ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
41 14 39 40 syl2anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
42 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
43 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
44 42 43 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
45 44 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
46 45 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
47 41 46 eqtrd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ 𝑁 ) )
48 lsw ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
49 48 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
50 fvoveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) )
51 50 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) )
52 19 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
53 52 43 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
54 53 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
55 51 54 sylan9eq ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
56 49 55 eqtrd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
57 47 56 preq12d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
58 57 eleq1d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
59 58 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
60 13 59 mpbird ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )
61 60 exp31 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
62 61 com23 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
63 62 3impia ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
64 4 63 syl ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
65 64 1 eleq2s ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
66 65 imp ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )