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∈NClWWalksNG→W++⟨“W⁡0”⟩∈w∈NWWalksNG|lastS⁡w=w⁡0

Proof

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