Metamath Proof Explorer


Theorem numclwwlkovh0

Description: Value of operation H , mapping a vertex v and an integer n greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) ... with v(n-2) =/= v" according to definition 7 in Huneke p. 2. (Contributed by AV, 1-May-2022)

Ref Expression
Hypothesis numclwwlkovh.h H=vV,n2wvClWWalksNOnGn|wn2v
Assertion numclwwlkovh0 XVN2XHN=wXClWWalksNOnGN|wN2X

Proof

Step Hyp Ref Expression
1 numclwwlkovh.h H=vV,n2wvClWWalksNOnGn|wn2v
2 oveq12 v=Xn=NvClWWalksNOnGn=XClWWalksNOnGN
3 oveq1 n=Nn2=N2
4 3 adantl v=Xn=Nn2=N2
5 4 fveq2d v=Xn=Nwn2=wN2
6 simpl v=Xn=Nv=X
7 5 6 neeq12d v=Xn=Nwn2vwN2X
8 2 7 rabeqbidv v=Xn=NwvClWWalksNOnGn|wn2v=wXClWWalksNOnGN|wN2X
9 ovex XClWWalksNOnGNV
10 9 rabex wXClWWalksNOnGN|wN2XV
11 8 1 10 ovmpoa XVN2XHN=wXClWWalksNOnGN|wN2X