Metamath Proof Explorer


Theorem wwlks

Description: The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Hypotheses wwlks.v V = Vtx G
wwlks.e E = Edg G
Assertion wwlks WWalks G = w Word V | w i 0 ..^ w 1 w i w i + 1 E

Proof

Step Hyp Ref Expression
1 wwlks.v V = Vtx G
2 wwlks.e E = Edg G
3 df-wwlks WWalks = g V w Word Vtx g | w i 0 ..^ w 1 w i w i + 1 Edg g
4 fveq2 g = G Vtx g = Vtx G
5 4 1 eqtr4di g = G Vtx g = V
6 wrdeq Vtx g = V Word Vtx g = Word V
7 5 6 syl g = G Word Vtx g = Word V
8 fveq2 g = G Edg g = Edg G
9 8 2 eqtr4di g = G Edg g = E
10 9 eleq2d g = G w i w i + 1 Edg g w i w i + 1 E
11 10 ralbidv g = G i 0 ..^ w 1 w i w i + 1 Edg g i 0 ..^ w 1 w i w i + 1 E
12 11 anbi2d g = G w i 0 ..^ w 1 w i w i + 1 Edg g w i 0 ..^ w 1 w i w i + 1 E
13 7 12 rabeqbidv g = G w Word Vtx g | w i 0 ..^ w 1 w i w i + 1 Edg g = w Word V | w i 0 ..^ w 1 w i w i + 1 E
14 id G V G V
15 1 fvexi V V
16 15 a1i G V V V
17 wrdexg V V Word V V
18 rabexg Word V V w Word V | w i 0 ..^ w 1 w i w i + 1 E V
19 16 17 18 3syl G V w Word V | w i 0 ..^ w 1 w i w i + 1 E V
20 3 13 14 19 fvmptd3 G V WWalks G = w Word V | w i 0 ..^ w 1 w i w i + 1 E
21 fvprc ¬ G V WWalks G =
22 fvprc ¬ G V Vtx G =
23 1 22 syl5eq ¬ G V V =
24 wrdeq V = Word V = Word
25 23 24 syl ¬ G V Word V = Word
26 25 eleq2d ¬ G V w Word V w Word
27 0wrd0 w Word w =
28 26 27 bitrdi ¬ G V w Word V w =
29 nne ¬ w w =
30 29 biimpri w = ¬ w
31 30 intnanrd w = ¬ w i 0 ..^ w 1 w i w i + 1 E
32 28 31 syl6bi ¬ G V w Word V ¬ w i 0 ..^ w 1 w i w i + 1 E
33 32 ralrimiv ¬ G V w Word V ¬ w i 0 ..^ w 1 w i w i + 1 E
34 rabeq0 w Word V | w i 0 ..^ w 1 w i w i + 1 E = w Word V ¬ w i 0 ..^ w 1 w i w i + 1 E
35 33 34 sylibr ¬ G V w Word V | w i 0 ..^ w 1 w i w i + 1 E =
36 21 35 eqtr4d ¬ G V WWalks G = w Word V | w i 0 ..^ w 1 w i w i + 1 E
37 20 36 pm2.61i WWalks G = w Word V | w i 0 ..^ w 1 w i w i + 1 E