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 syl6bir 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