Metamath Proof Explorer

Theorem 2clwwlk

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 ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
Assertion 2clwwlk ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X

Proof

Step Hyp Ref Expression
1 2clwwlk.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ 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 ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
8 ovex ⊢ X ClWWalksNOn ⁡ G N ∈ V
9 8 rabex ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X ∈ V
10 7 1 9 ovmpoa ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X