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∈nWWalksNG|w⁡0=v∧lastS⁡w≠v
Assertion numclwwlkovq ⊢X∈V∧N∈ℕ→XQN=w∈NWWalksNG|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∈nWWalksNG|w⁡0=v∧lastS⁡w≠v
3 oveq1 ⊢n=N→nWWalksNG=NWWalksNG
4 3 adantl ⊢v=X∧n=N→nWWalksNG=NWWalksNG
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∈nWWalksNG|w⁡0=v∧lastS⁡w≠v=w∈NWWalksNG|w⁡0=X∧lastS⁡w≠X
10 ovex ⊢NWWalksNG∈V
11 10 rabex ⊢w∈NWWalksNG|w⁡0=X∧lastS⁡w≠X∈V
12 9 2 11 ovmpoa ⊢X∈V∧N∈ℕ→XQN=w∈NWWalksNG|w⁡0=X∧lastS⁡w≠X