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 ⊢ V = Vtx ⁡ G
wwlknp.e ⊢ E = Edg ⁡ G
Assertion wwlknp ⊢ W ∈ N WWalksN G → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E

Proof

Step Hyp Ref Expression
1 wwlkbp.v ⊢ V = Vtx ⁡ G
2 wwlknp.e ⊢ E = Edg ⁡ G
3 1 wwlknbp ⊢ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V
4 iswwlksn ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
5 1 2 iswwlks ⊢ W ∈ WWalks ⁡ G ↔ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
6 simpl2 ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1 ∧ N ∈ ℕ 0 → W ∈ Word V
7 simprl ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1 ∧ N ∈ ℕ 0 → W = N + 1
8 oveq1 ⊢ W = N + 1 → W − 1 = N + 1 - 1
9 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
10 pncan1 ⊢ N ∈ ℂ → N + 1 - 1 = N
11 9 10 syl ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
12 8 11 sylan9eq ⊢ W = N + 1 ∧ N ∈ ℕ 0 → W − 1 = N
13 12 oveq2d ⊢ W = N + 1 ∧ N ∈ ℕ 0 → 0 ..^ W − 1 = 0 ..^ N
14 13 raleqdv ⊢ W = N + 1 ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ↔ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
15 14 biimpcd ⊢ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E → W = N + 1 ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
16 15 3ad2ant3 ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E → W = N + 1 ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
17 16 imp ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1 ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
18 6 7 17 3jca ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1 ∧ N ∈ ℕ 0 → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
19 18 ex ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E → W = N + 1 ∧ N ∈ ℕ 0 → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
20 5 19 sylbi ⊢ W ∈ WWalks ⁡ G → W = N + 1 ∧ N ∈ ℕ 0 → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
21 20 expdimp ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 → N ∈ ℕ 0 → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
22 21 com12 ⊢ N ∈ ℕ 0 → W ∈ WWalks ⁡ G ∧ W = N + 1 → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
23 4 22 sylbid ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
24 23 3ad2ant2 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V → W ∈ N WWalksN G → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E
25 3 24 mpcom ⊢ W ∈ N WWalksN G → W ∈ Word V ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ E