Metamath Proof Explorer

Theorem clwwlknwwlkncl

Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlknwwlkncl ⊢ W ∈ N ClWWalksN G → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0

Proof

Step Hyp Ref Expression
1 clwwlknnn ⊢ W ∈ N ClWWalksN G → N ∈ ℕ
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 clwwlknbp ⊢ W ∈ N ClWWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N
4 eqid ⊢ Edg ⁡ G = Edg ⁡ G
5 2 4 clwwlknp ⊢ W ∈ N ClWWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
6 3simpc ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
7 5 6 syl ⊢ W ∈ N ClWWalksN G → ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
8 eqid ⊢ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0
9 8 clwwlkel ⊢ N ∈ ℕ ∧ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0
10 1 3 7 9 syl3anc ⊢ W ∈ N ClWWalksN G → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0