Metamath Proof Explorer

Theorem numclwwlkovq

Description: Value of operation Q , mapping a vertex v and a positive integer n to the not closed walks v(0) ... v(n) of length n from a fixed vertex v = v(0). "Not closed" means v(n) =/= v(0). Remark: n e. NN0 would not be useful: numclwwlkqhash would not hold, because ( K ^ 0 ) = 1 ! (Contributed by Alexander van der Vekens, 27-Sep-2018) (Revised by AV, 30-May-2021)

Ref Expression
Hypotheses numclwwlk.v ⊢ V = Vtx ⁡ G
numclwwlk.q ⊢ Q = v ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
Assertion numclwwlkovq ⊢ X ∈ V ∧ N ∈ ℕ → X Q N = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢ V = Vtx ⁡ G
2 numclwwlk.q ⊢ Q = v ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
3 oveq1 ⊢ n = N → n WWalksN G = N WWalksN G
4 3 adantl ⊢ v = X ∧ n = N → n WWalksN G = N WWalksN G
5 eqeq2 ⊢ v = X → w ⁡ 0 = v ↔ w ⁡ 0 = X
6 neeq2 ⊢ v = X → lastS ⁡ w ≠ v ↔ lastS ⁡ w ≠ X
7 5 6 anbi12d ⊢ v = X → w ⁡ 0 = v ∧ lastS ⁡ w ≠ v ↔ w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
8 7 adantr ⊢ v = X ∧ n = N → w ⁡ 0 = v ∧ lastS ⁡ w ≠ v ↔ w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
9 4 8 rabeqbidv ⊢ v = X ∧ n = N → w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
10 ovex ⊢ N WWalksN G ∈ V
11 10 rabex ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X ∈ V
12 9 2 11 ovmpoa ⊢ X ∈ V ∧ N ∈ ℕ → X Q N = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X