Metamath Proof Explorer

Theorem wwlknp

Description: Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Hypotheses wwlkbp.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlknp.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlknp ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 wwlkbp.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlknp.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 wwlknbp ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) )
4 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )
5 1 2 iswwlks ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
6 simpl2 ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → 𝑊 ∈ Word 𝑉 )
7 simprl ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) )
8 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
9 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
10 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
11 9 10 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
12 8 11 sylan9eq ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
13 12 oveq2d ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
14 13 raleqdv ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
15 14 biimpcd ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
16 15 3ad2ant3 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
17 16 imp ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
18 6 7 17 3jca ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
19 18 ex ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
20 5 19 sylbi ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
21 20 expdimp ⊢ ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
22 21 com12 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
23 4 22 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
24 23 3ad2ant2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
25 3 24 mpcom ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )