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 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
23 1red ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
24 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
25 23 24 addge02d ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ≤ 𝑁 ↔ 1 ≤ ( 𝑁 + 1 ) ) )
26 22 25 mpbid ⊢ ( 𝑁 ∈ ℕ0 → 1 ≤ ( 𝑁 + 1 ) )
27 26 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ ( 𝑁 + 1 ) )
28 19 nn0red ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
29 28 lep1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
30 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
31 29 30 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
32 31 a1i ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
33 32 com23 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
34 16 33 syl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
35 34 imp31 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) )
36 15 18 21 27 35 elfzd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
37 pfxfvlsw ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
38 14 36 37 syl2anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
39 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
40 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
41 39 40 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
42 41 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
43 42 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
44 38 43 eqtrd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ 𝑁 ) )
45 lsw ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
46 45 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
47 fvoveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) )
48 47 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) )
49 19 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
50 49 40 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
51 50 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
52 48 51 sylan9eq ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
53 46 52 eqtrd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
54 44 53 preq12d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
55 54 eleq1d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
56 55 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
57 13 56 mpbird ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )
58 57 exp31 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
59 58 com23 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
60 59 3impia ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
61 4 60 syl ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
62 61 1 eleq2s ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑁 ∈ ℕ0 → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
63 62 imp ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )