Metamath Proof Explorer

Theorem clwwlknonwwlknonb

Description: A word over vertices represents a closed walk of a fixed length N on vertex X iff the word concatenated with X represents a walk of length N on X and X . This theorem would not hold for N = 0 and W = (/) , see clwwlknwwlksnb . (Contributed by AV, 4-Mar-2022) (Revised by AV, 27-Mar-2022)

Ref Expression
Hypothesis clwwlknonwwlknonb.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clwwlknonwwlknonb ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 clwwlknonwwlknonb.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isclwwlknon ⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )
3 3anan32 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) )
4 s1eq ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ⟨“ 𝑋 ”⟩ )
5 4 oveq2d ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) )
6 5 eleq1d ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
7 6 biimpac ⊢ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) )
8 7 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) )
9 fvex ⊢ ( 𝑊 ‘ 0 ) ∈ V
10 eleq1 ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ‘ 0 ) ∈ V ↔ 𝑋 ∈ V ) )
11 9 10 mpbii ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → 𝑋 ∈ V )
12 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
13 1 12 wwlknp ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
14 simprrl ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) ) → 𝑊 ∈ Word 𝑉 )
15 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑊 ∈ Word 𝑉 )
16 15 anim2i ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑋 ∈ V ∧ 𝑊 ∈ Word 𝑉 ) )
17 16 ancomd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ V ) )
18 ccats1alpha ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ V ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) )
19 17 18 syl ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) )
20 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
21 19 20 syl6bi ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 → 𝑋 ∈ 𝑉 ) )
22 21 com12 ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → 𝑋 ∈ 𝑉 ) )
23 22 adantr ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → 𝑋 ∈ 𝑉 ) )
24 23 imp ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) ) → 𝑋 ∈ 𝑉 )
25 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
26 ccatws1lenp1b ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
27 25 26 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
28 27 biimpd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
29 28 adantl ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
30 29 com12 ⊢ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
31 30 adantl ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
32 31 imp ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
33 32 eqcomd ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) ) → 𝑁 = ( ♯ ‘ 𝑊 ) )
34 14 24 33 3jca ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) )
35 34 ex ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) )
36 35 3adant3 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) )
37 13 36 syl ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑋 ∈ V ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) )
38 37 expd ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑋 ∈ V → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) ) )
39 11 38 syl5com ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) ) )
40 6 39 sylbid ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) ) )
41 40 com13 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ‘ 0 ) = 𝑋 → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) ) )
42 41 imp32 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) )
43 ccats1val2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 )
44 42 43 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 )
45 ccat1st1st ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
46 45 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
47 5 fveq1d ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) )
48 47 eqeq1d ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
49 48 adantl ⊢ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
50 46 49 syl5ibcom ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
51 50 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
52 simprr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( 𝑊 ‘ 0 ) = 𝑋 )
53 51 52 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 )
54 8 44 53 jca31 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) )
55 54 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) ) )
56 simprl ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → 𝑊 ∈ Word 𝑉 )
57 27 biimpcd ⊢ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
58 57 adantl ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
59 58 imp ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
60 59 eqcomd ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → 𝑁 = ( ♯ ‘ 𝑊 ) )
61 56 60 jca ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) )
62 61 ex ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) )
63 62 3adant3 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) )
64 13 63 syl ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) ) )
65 64 imp ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) )
66 eleq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
67 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
68 67 biimpri ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
69 66 68 syl6bi ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
70 69 com12 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = ( ♯ ‘ 𝑊 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
71 70 ad2antll ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑁 = ( ♯ ‘ 𝑊 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
72 71 anim2d ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) )
73 65 72 mpd ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
74 ccats1val1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
75 73 74 syl ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
76 75 eqeq1d ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ↔ ( 𝑊 ‘ 0 ) = 𝑋 ) )
77 76 biimpd ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 → ( 𝑊 ‘ 0 ) = 𝑋 ) )
78 77 ex ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 → ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
79 78 adantr ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 → ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
80 79 com3r ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
81 80 impcom ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ‘ 0 ) = 𝑋 ) )
82 6 biimparc ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) )
83 simpr ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ‘ 0 ) = 𝑋 )
84 82 83 jca ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )
85 84 ex ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
86 85 ad2antrr ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) → ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
87 81 86 syldc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
88 55 87 impbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ) ) )
89 3 88 bitr4id ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ↔ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
90 1 clwwlknwwlksnb ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
91 90 anbi1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ↔ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
92 89 91 bitr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
93 2 92 bitr4id ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) ) )
94 wwlknon ⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 ) )
95 93 94 bitr4di ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) )