Metamath Proof Explorer

Theorem wwlksnwwlksnon

Description: A walk of fixed length is a walk of fixed length between two vertices. (Contributed by Alexander van der Vekens, 21-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 13-Mar-2022)

Ref Expression
Hypothesis wwlksnwwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wwlksnwwlksnon ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )

Proof

Step Hyp Ref Expression
1 wwlksnwwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlknbp1 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
3 1 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
4 3 wrdeqi ⊢ Word ( Vtx ‘ 𝐺 ) = Word 𝑉
5 4 eleq2i ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑊 ∈ Word 𝑉 )
6 5 biimpi ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 )
7 6 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word 𝑉 )
8 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
9 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑁 + 1 ) ∈ ℕ )
10 8 9 sylibr ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
11 10 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
12 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
13 12 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
14 13 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
15 11 14 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 15 adantl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
17 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
18 7 16 17 syl2an2 ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
19 fzonn0p1 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
21 12 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
22 21 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
23 20 22 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
24 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 )
25 7 23 24 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 )
26 25 adantl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 )
27 simpl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
28 eqidd ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
29 eqidd ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) )
30 eqeq2 ⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ↔ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
31 30 3anbi2d ⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) )
32 eqeq2 ⊢ ( 𝑏 = ( 𝑊 ‘ 𝑁 ) → ( ( 𝑊 ‘ 𝑁 ) = 𝑏 ↔ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) )
33 32 3anbi3d ⊢ ( 𝑏 = ( 𝑊 ‘ 𝑁 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) ) )
34 31 33 rspc2ev ⊢ ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) )
35 18 26 27 28 29 34 syl113anc ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) )
36 2 35 mpdan ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) )
37 simp1 ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
38 37 a1i ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
39 38 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
40 36 39 impbii ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) )
41 wwlknon ⊢ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) )
42 41 bicomi ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )
43 42 2rexbii ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )
44 40 43 bitri ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )