Metamath Proof Explorer

Theorem clwwlknwwlksnb

Description: A word over vertices represents a closed walk of a fixed length N greater than zero iff the word concatenated with its first symbol represents a walk of length N . This theorem would not hold for N = 0 and W = (/) , because ( W ++ <" ( W0 ) "> ) = <" (/) "> e. ( 0 WWalksN G ) could be true, but not W e. ( 0 ClWWalksN G ) <-> (/) e. (/) . (Contributed by AV, 4-Mar-2022) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypothesis clwwlkwwlksb.v ⊢ V = Vtx ⁡ G
Assertion clwwlknwwlksnb ⊢ W ∈ Word V ∧ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ N WWalksN G

Proof

Step Hyp Ref Expression
1 clwwlkwwlksb.v ⊢ V = Vtx ⁡ G
2 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
3 ccatws1lenp1b ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W ++ ⟨“ W ⁡ 0 ”⟩ = N + 1 ↔ W = N
4 2 3 sylan2 ⊢ W ∈ Word V ∧ N ∈ ℕ → W ++ ⟨“ W ⁡ 0 ”⟩ = N + 1 ↔ W = N
5 4 anbi2d ⊢ W ∈ Word V ∧ N ∈ ℕ → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ∧ W ++ ⟨“ W ⁡ 0 ”⟩ = N + 1 ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ∧ W = N
6 simpl ⊢ W ∈ Word V ∧ N ∈ ℕ → W ∈ Word V
7 eleq1 ⊢ W = N → W ∈ ℕ ↔ N ∈ ℕ
8 len0nnbi ⊢ W ∈ Word V → W ≠ ∅ ↔ W ∈ ℕ
9 8 biimprcd ⊢ W ∈ ℕ → W ∈ Word V → W ≠ ∅
10 7 9 biimtrrdi ⊢ W = N → N ∈ ℕ → W ∈ Word V → W ≠ ∅
11 10 com13 ⊢ W ∈ Word V → N ∈ ℕ → W = N → W ≠ ∅
12 11 imp31 ⊢ W ∈ Word V ∧ N ∈ ℕ ∧ W = N → W ≠ ∅
13 1 clwwlkwwlksb ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ClWWalks ⁡ G ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G
14 6 12 13 syl2an2r ⊢ W ∈ Word V ∧ N ∈ ℕ ∧ W = N → W ∈ ClWWalks ⁡ G ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G
15 14 bicomd ⊢ W ∈ Word V ∧ N ∈ ℕ ∧ W = N → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ↔ W ∈ ClWWalks ⁡ G
16 15 ex ⊢ W ∈ Word V ∧ N ∈ ℕ → W = N → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ↔ W ∈ ClWWalks ⁡ G
17 16 pm5.32rd ⊢ W ∈ Word V ∧ N ∈ ℕ → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ∧ W = N ↔ W ∈ ClWWalks ⁡ G ∧ W = N
18 5 17 bitrd ⊢ W ∈ Word V ∧ N ∈ ℕ → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ∧ W ++ ⟨“ W ⁡ 0 ”⟩ = N + 1 ↔ W ∈ ClWWalks ⁡ G ∧ W = N
19 2 adantl ⊢ W ∈ Word V ∧ N ∈ ℕ → N ∈ ℕ 0
20 iswwlksn ⊢ N ∈ ℕ 0 → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ N WWalksN G ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ∧ W ++ ⟨“ W ⁡ 0 ”⟩ = N + 1
21 19 20 syl ⊢ W ∈ Word V ∧ N ∈ ℕ → W ++ ⟨“ W ⁡ 0 ”⟩ ∈ N WWalksN G ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ WWalks ⁡ G ∧ W ++ ⟨“ W ⁡ 0 ”⟩ = N + 1
22 isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
23 22 a1i ⊢ W ∈ Word V ∧ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
24 18 21 23 3bitr4rd ⊢ W ∈ Word V ∧ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ N WWalksN G