Metamath Proof Explorer

Theorem wwlksnextproplem1

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

Ref Expression
Hypothesis wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
Assertion wwlksnextproplem1 ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
2 wwlknbp1 ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) )
3 simpl2 ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
4 peano2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
5 4 3ad2ant1 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
6 eleq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ) )
7 6 3ad2ant3 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ) )
8 5 7 mpbird ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9 8 adantr ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
10 simpr ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
11 nn0re ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
12 11 lep1d ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
13 12 3ad2ant1 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
14 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
15 14 3ad2ant3 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
16 13 15 mpbird ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) )
17 16 adantr ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) )
18 nn0p1elfzo ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
19 10 9 17 18 syl3anc ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 fz0add1fz1 ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
21 9 19 20 syl2anc ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
22 3 21 jca ⊢ ( ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
23 22 ex ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) ) )
24 2 23 syl ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) ) )
25 24 1 eleq2s ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) ) )
26 25 imp ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
27 pfxfv0 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
28 26 27 syl ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )