Description: The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | wwlksn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | |
|
2 | 1 | adantl | |
3 | oveq1 | |
|
4 | 3 | eqeq2d | |
5 | 4 | adantr | |
6 | 2 5 | rabeqbidv | |
7 | df-wwlksn | |
|
8 | fvex | |
|
9 | 8 | rabex | |
10 | 6 7 9 | ovmpoa | |
11 | 10 | expcom | |
12 | 7 | reldmmpo | |
13 | 12 | ovprc2 | |
14 | fvprc | |
|
15 | 14 | rabeqdv | |
16 | rab0 | |
|
17 | 15 16 | eqtrdi | |
18 | 13 17 | eqtr4d | |
19 | 18 | a1d | |
20 | 11 19 | pm2.61i | |