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 | |
|
Assertion | numclwwlkovh0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | numclwwlkovh.h | |
|
2 | oveq12 | |
|
3 | oveq1 | |
|
4 | 3 | adantl | |
5 | 4 | fveq2d | |
6 | simpl | |
|
7 | 5 6 | neeq12d | |
8 | 2 7 | rabeqbidv | |
9 | ovex | |
|
10 | 9 | rabex | |
11 | 8 1 10 | ovmpoa | |