Metamath Proof Explorer


Theorem iswwlksn

Description: A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion iswwlksn N 0 W N WWalksN G W WWalks G W = N + 1

Proof

Step Hyp Ref Expression
1 wwlksn N 0 N WWalksN G = w WWalks G | w = N + 1
2 1 eleq2d N 0 W N WWalksN G W w WWalks G | w = N + 1
3 fveqeq2 w = W w = N + 1 W = N + 1
4 3 elrab W w WWalks G | w = N + 1 W WWalks G W = N + 1
5 2 4 bitrdi N 0 W N WWalksN G W WWalks G W = N + 1