Metamath Proof Explorer

Theorem numclwwlkovh

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. Definition of ClWWalksNOn resolved. (Contributed by Alexander van der Vekens, 26-Aug-2018) (Revised by AV, 30-May-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypothesis numclwwlkovh.h ⊢H=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2≠v
Assertion numclwwlkovh ⊢X∈V∧N∈ℤ≥2→XHN=w∈NClWWalksNG|w⁡0=X∧w⁡N−2≠w⁡0

Proof

Step Hyp Ref Expression
1 numclwwlkovh.h ⊢H=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2≠v
2 1 numclwwlkovh0 ⊢X∈V∧N∈ℤ≥2→XHN=w∈XClWWalksNOn⁡GN|w⁡N−2≠X
3 isclwwlknon ⊢w∈XClWWalksNOn⁡GN↔w∈NClWWalksNG∧w⁡0=X
4 3 anbi1i ⊢w∈XClWWalksNOn⁡GN∧w⁡N−2≠X↔w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X
5 simpll ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X→w∈NClWWalksNG
6 simplr ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X→w⁡0=X
7 neeq2 ⊢X=w⁡0→w⁡N−2≠X↔w⁡N−2≠w⁡0
8 7 eqcoms ⊢w⁡0=X→w⁡N−2≠X↔w⁡N−2≠w⁡0
9 8 adantl ⊢w∈NClWWalksNG∧w⁡0=X→w⁡N−2≠X↔w⁡N−2≠w⁡0
10 9 biimpa ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X→w⁡N−2≠w⁡0
11 6 10 jca ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X→w⁡0=X∧w⁡N−2≠w⁡0
12 5 11 jca ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X→w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠w⁡0
13 simpl ⊢w⁡0=X∧w⁡N−2≠w⁡0→w⁡0=X
14 13 anim2i ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠w⁡0→w∈NClWWalksNG∧w⁡0=X
15 neeq2 ⊢w⁡0=X→w⁡N−2≠w⁡0↔w⁡N−2≠X
16 15 biimpa ⊢w⁡0=X∧w⁡N−2≠w⁡0→w⁡N−2≠X
17 16 adantl ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠w⁡0→w⁡N−2≠X
18 14 17 jca ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠w⁡0→w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X
19 12 18 impbii ⊢w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠X↔w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠w⁡0
20 4 19 bitri ⊢w∈XClWWalksNOn⁡GN∧w⁡N−2≠X↔w∈NClWWalksNG∧w⁡0=X∧w⁡N−2≠w⁡0
21 20 rabbia2 ⊢w∈XClWWalksNOn⁡GN|w⁡N−2≠X=w∈NClWWalksNG|w⁡0=X∧w⁡N−2≠w⁡0
22 2 21 eqtrdi ⊢X∈V∧N∈ℤ≥2→XHN=w∈NClWWalksNG|w⁡0=X∧w⁡N−2≠w⁡0