Metamath Proof Explorer


Theorem clwwlknonel

Description: Characterization of a word over the set of vertices representing a closed walk on vertex X of (nonzero) length N in a graph G . This theorem would not hold for N = 0 if W = X = (/) . (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 clwwlknonel.v V = Vtx G
2 clwwlknonel.e E = Edg G
3 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
4 simpl W = N W = W = N
5 fveq2 W = W =
6 hash0 = 0
7 5 6 syl6eq W = W = 0
8 7 adantl W = N W = W = 0
9 4 8 eqtr3d W = N W = N = 0
10 9 ex W = N W = N = 0
11 10 necon3d W = N N 0 W
12 11 impcom N 0 W = N W
13 12 biantrud N 0 W = N W Word V W Word V W
14 13 bicomd N 0 W = N W Word V W W Word V
15 14 3anbi1d N 0 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
16 3 15 syl5bb N 0 W = N W ClWWalks G W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
17 16 a1d N 0 W = N W 0 = X W ClWWalks G W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
18 17 expimpd N 0 W = N W 0 = X W ClWWalks G W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E
19 18 pm5.32rd N 0 W ClWWalks G W = N W 0 = X W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N W 0 = X
20 isclwwlknon W X ClWWalksNOn G N W N ClWWalksN G W 0 = X
21 isclwwlkn W N ClWWalksN G W ClWWalks G W = N
22 21 anbi1i W N ClWWalksN G W 0 = X W ClWWalks G W = N W 0 = X
23 anass W ClWWalks G W = N W 0 = X W ClWWalks G W = N W 0 = X
24 20 22 23 3bitri W X ClWWalksNOn G N W ClWWalks G W = N W 0 = X
25 3anass W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N W 0 = X W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N W 0 = X
26 19 24 25 3bitr4g N 0 W X ClWWalksNOn G N W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N W 0 = X