This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clwwlknwwlksnb ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )

Proof

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