Description: Value of operation C , 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 6 in Huneke p. 2. Such closed walks are "double loops" consisting of a closed (n-2)-walk v = v(0) ... v(n-2) = v and a closed 2-walk v = v(n-2) v(n-1) v(n) = v, see 2clwwlk2clwwlk . ( X C N ) is called the "set of double loops of length N on vertex X " in the following. (Contributed by Alexander van der Vekens, 14-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 20-Apr-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 2clwwlk.c | |- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) |
|
| Assertion | 2clwwlk | |- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2clwwlk.c | |- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) |
|
| 2 | oveq12 | |- ( ( v = X /\ n = N ) -> ( v ( ClWWalksNOn ` G ) n ) = ( X ( ClWWalksNOn ` G ) N ) ) |
|
| 3 | fvoveq1 | |- ( n = N -> ( w ` ( n - 2 ) ) = ( w ` ( N - 2 ) ) ) |
|
| 4 | 3 | adantl | |- ( ( v = X /\ n = N ) -> ( w ` ( n - 2 ) ) = ( w ` ( N - 2 ) ) ) |
| 5 | simpl | |- ( ( v = X /\ n = N ) -> v = X ) |
|
| 6 | 4 5 | eqeq12d | |- ( ( v = X /\ n = N ) -> ( ( w ` ( n - 2 ) ) = v <-> ( w ` ( N - 2 ) ) = X ) ) |
| 7 | 2 6 | rabeqbidv | |- ( ( v = X /\ n = N ) -> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) |
| 8 | ovex | |- ( X ( ClWWalksNOn ` G ) N ) e. _V |
|
| 9 | 8 | rabex | |- { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. _V |
| 10 | 7 1 9 | ovmpoa | |- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) |