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

Proof

Step Hyp Ref Expression
1 numclwwlkovh.h ⊢ H = 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 oveq1 ⊢ n = N → n − 2 = N − 2
4 3 adantl ⊢ v = X ∧ n = N → n − 2 = N − 2
5 4 fveq2d ⊢ v = X ∧ n = N → w ⁡ n − 2 = w ⁡ N − 2
6 simpl ⊢ v = X ∧ n = N → v = X
7 5 6 neeq12d ⊢ v = X ∧ n = N → w ⁡ n − 2 ≠ v ↔ w ⁡ N − 2 ≠ X
8 2 7 rabeqbidv ⊢ v = X ∧ n = N → w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X
9 ovex ⊢ X ClWWalksNOn ⁡ G N ∈ V
10 9 rabex ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∈ V
11 8 1 10 ovmpoa ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X