Metamath Proof Explorer


Theorem isclwwlknx

Description: Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v V = Vtx G
isclwwlknx.e E = Edg G
Assertion isclwwlknx N W N ClWWalksN G W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N

Proof

Step Hyp Ref Expression
1 isclwwlknx.v V = Vtx G
2 isclwwlknx.e E = Edg G
3 eleq1 W = N W N
4 len0nnbi W Word V W W
5 4 biimprcd W W Word V W
6 3 5 syl6bir W = N N W Word V W
7 6 impcom N W = N W Word V W
8 7 imp N W = N W Word V W
9 8 biantrurd N W = N W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
10 9 bicomd N W = N W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
11 10 pm5.32da N W = N W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
12 11 ex N W = N W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
13 12 pm5.32rd N W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N
14 isclwwlkn W N ClWWalksN G W ClWWalks G W = N
15 1 2 isclwwlk W ClWWalks G W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
16 3anass W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
17 anass W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
18 16 17 bitri W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
19 15 18 bitri W ClWWalks G W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
20 19 anbi1i W ClWWalks G W = N W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N
21 14 20 bitri W N ClWWalksN G W Word V W i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N
22 3anass W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
23 22 anbi1i W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N
24 13 21 23 3bitr4g N W N ClWWalksN G W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N