Metamath Proof Explorer


Theorem clwwlkn2

Description: A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Assertion clwwlkn2 W 2 ClWWalksN G W = 2 W Word Vtx G W 0 W 1 Edg G

Proof

Step Hyp Ref Expression
1 2nn 2
2 eqid Vtx G = Vtx G
3 eqid Edg G = Edg G
4 2 3 isclwwlknx 2 W 2 ClWWalksN G W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W = 2
5 1 4 ax-mp W 2 ClWWalksN G W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W = 2
6 3anass W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G
7 oveq1 W = 2 W 1 = 2 1
8 2m1e1 2 1 = 1
9 7 8 eqtrdi W = 2 W 1 = 1
10 9 oveq2d W = 2 0 ..^ W 1 = 0 ..^ 1
11 fzo01 0 ..^ 1 = 0
12 10 11 eqtrdi W = 2 0 ..^ W 1 = 0
13 12 adantr W = 2 W Word Vtx G 0 ..^ W 1 = 0
14 13 raleqdv W = 2 W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G i 0 W i W i + 1 Edg G
15 c0ex 0 V
16 fveq2 i = 0 W i = W 0
17 fv0p1e1 i = 0 W i + 1 = W 1
18 16 17 preq12d i = 0 W i W i + 1 = W 0 W 1
19 18 eleq1d i = 0 W i W i + 1 Edg G W 0 W 1 Edg G
20 15 19 ralsn i 0 W i W i + 1 Edg G W 0 W 1 Edg G
21 14 20 bitrdi W = 2 W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G W 0 W 1 Edg G
22 prcom lastS W W 0 = W 0 lastS W
23 lsw W Word Vtx G lastS W = W W 1
24 9 fveq2d W = 2 W W 1 = W 1
25 23 24 sylan9eqr W = 2 W Word Vtx G lastS W = W 1
26 25 preq2d W = 2 W Word Vtx G W 0 lastS W = W 0 W 1
27 22 26 syl5eq W = 2 W Word Vtx G lastS W W 0 = W 0 W 1
28 27 eleq1d W = 2 W Word Vtx G lastS W W 0 Edg G W 0 W 1 Edg G
29 21 28 anbi12d W = 2 W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W 0 W 1 Edg G W 0 W 1 Edg G
30 anidm W 0 W 1 Edg G W 0 W 1 Edg G W 0 W 1 Edg G
31 29 30 bitrdi W = 2 W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W 0 W 1 Edg G
32 31 pm5.32da W = 2 W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W Word Vtx G W 0 W 1 Edg G
33 6 32 syl5bb W = 2 W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W Word Vtx G W 0 W 1 Edg G
34 33 pm5.32ri W Word Vtx G i 0 ..^ W 1 W i W i + 1 Edg G lastS W W 0 Edg G W = 2 W Word Vtx G W 0 W 1 Edg G W = 2
35 3anass W = 2 W Word Vtx G W 0 W 1 Edg G W = 2 W Word Vtx G W 0 W 1 Edg G
36 ancom W = 2 W Word Vtx G W 0 W 1 Edg G W Word Vtx G W 0 W 1 Edg G W = 2
37 35 36 bitr2i W Word Vtx G W 0 W 1 Edg G W = 2 W = 2 W Word Vtx G W 0 W 1 Edg G
38 5 34 37 3bitri W 2 ClWWalksN G W = 2 W Word Vtx G W 0 W 1 Edg G