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 ‘ 𝑊 ) } ∈ 𝐸 )