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

Metamath Proof Explorer

Theorem clwwlkwwlksb

Description: A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022)

Ref Expression
Hypothesis clwwlkwwlksb.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clwwlkwwlksb ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkwwlksb.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fstwrdne ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
3 2 s1cld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 )
4 ccatlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) )
5 3 4 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) )
6 s1len ⊢ ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = 1
7 6 oveq2i ⊢ ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 )
8 5 7 eqtrdi ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
9 8 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
10 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
12 11 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
13 1cnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 1 ∈ ℂ )
14 12 13 13 addsubd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) )
15 9 14 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) )
16 15 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) )
17 16 raleqdv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
18 lennncl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
19 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
20 18 19 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
21 elnn0uz ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
22 20 21 sylib ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
23 fzosplitsn ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
24 22 23 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
25 24 raleqdv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
26 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
27 25 26 bitrdi ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
28 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 𝑊 ∈ Word 𝑉 )
29 10 nn0zd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
30 29 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
31 elfzom1elfzo ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
32 30 31 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
33 ccats1val1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
34 28 32 33 syl2an2r ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
35 elfzom1elp1fzo ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
36 30 35 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
37 ccats1val1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
38 28 36 37 syl2an2r ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
39 34 38 preq12d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } )
40 39 eleq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
41 40 ralbidva ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
42 ovex ⊢ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ V
43 fveq2 ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
44 fvoveq1 ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) )
45 43 44 preq12d ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } )
46 45 eleq1d ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
47 42 46 ralsn ⊢ ( ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
48 fzo0end ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
49 18 48 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
50 ccats1val1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
51 49 50 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
52 lsw ⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
53 52 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
54 51 53 eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
55 npcan1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
56 11 55 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
57 56 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
58 57 fveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) )
59 eqidd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
60 ccats1val2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = ( 𝑊 ‘ 0 ) )
61 28 2 59 60 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = ( 𝑊 ‘ 0 ) )
62 58 61 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( 𝑊 ‘ 0 ) )
63 54 62 preq12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } = { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } )
64 63 eleq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
65 47 64 bitrid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
66 41 65 anbi12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
67 17 27 66 3bitrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
68 28 3 jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) )
69 ccat0 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = ∅ ↔ ( 𝑊 = ∅ ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ∅ ) ) )
70 simpl ⊢ ( ( 𝑊 = ∅ ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ∅ ) → 𝑊 = ∅ )
71 69 70 biimtrdi ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = ∅ → 𝑊 = ∅ ) )
72 71 necon3d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( 𝑊 ≠ ∅ → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ) )
73 72 adantld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ) )
74 68 73 mpcom ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ )
75 wrdv ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V )
76 s1cli ⊢ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word V
77 ccatalpha ⊢ ( ( 𝑊 ∈ Word V ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word V ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) ) )
78 75 76 77 sylancl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) ) )
79 78 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) ) )
80 28 3 79 mpbir2and ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 )
81 74 80 jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) )
82 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
83 1 82 iswwlks ⊢ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
84 df-3an ⊢ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
85 83 84 bitri ⊢ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
86 85 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
87 81 86 mpbirand ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
88 1 82 isclwwlk ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
89 3anass ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
90 88 89 bitri ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
91 90 baib ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
92 67 87 91 3bitr4rd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ) )