Metamath Proof Explorer

Theorem wwlknbp

Description: Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018) (Revised by AV, 9-Apr-2021) (Proof shortened by AV, 20-May-2021)

Ref Expression
Hypothesis wwlkbp.v ⊢ V = Vtx ⁡ G
Assertion wwlknbp ⊢ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V

Proof

Step Hyp Ref Expression
1 wwlkbp.v ⊢ V = Vtx ⁡ G
2 df-wwlksn ⊢ WWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1
3 2 elmpocl ⊢ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ G ∈ V
4 simpl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ G ∈ V
5 4 ancomd ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0
6 iswwlksn ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
7 6 adantr ⊢ N ∈ ℕ 0 ∧ G ∈ V → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
8 1 wwlkbp ⊢ W ∈ WWalks ⁡ G → G ∈ V ∧ W ∈ Word V
9 8 simprd ⊢ W ∈ WWalks ⁡ G → W ∈ Word V
10 9 adantr ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 → W ∈ Word V
11 7 10 syl6bi ⊢ N ∈ ℕ 0 ∧ G ∈ V → W ∈ N WWalksN G → W ∈ Word V
12 11 imp ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G → W ∈ Word V
13 df-3an ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V ↔ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V
14 5 12 13 sylanbrc ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V
15 3 14 mpancom ⊢ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V