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

Proof

Step Hyp Ref Expression
1 numclwwlkovh.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
2 1 numclwwlkovh0 ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X
3 isclwwlknon ⊢ w ∈ X ClWWalksNOn ⁡ G N ↔ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X
4 3 anbi1i ⊢ w ∈ X ClWWalksNOn ⁡ G N ∧ w ⁡ N − 2 ≠ X ↔ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X
5 simpll ⊢ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X → w ∈ N ClWWalksN G
6 simplr ⊢ w ∈ N ClWWalksN G ∧ 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 ∈ N ClWWalksN G ∧ w ⁡ 0 = X → w ⁡ N − 2 ≠ X ↔ w ⁡ N − 2 ≠ w ⁡ 0
10 9 biimpa ⊢ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X → w ⁡ N − 2 ≠ w ⁡ 0
11 6 10 jca ⊢ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X → w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0
12 5 11 jca ⊢ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X → w ∈ N ClWWalksN G ∧ 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 ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0 → w ∈ N ClWWalksN G ∧ 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 ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0 → w ⁡ N − 2 ≠ X
18 14 17 jca ⊢ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0 → w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X
19 12 18 impbii ⊢ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ X ↔ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0
20 4 19 bitri ⊢ w ∈ X ClWWalksNOn ⁡ G N ∧ w ⁡ N − 2 ≠ X ↔ w ∈ N ClWWalksN G ∧ w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0
21 20 rabbia2 ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X = w ∈ N ClWWalksN G | w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0
22 2 21 eqtrdi ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N = w ∈ N ClWWalksN G | w ⁡ 0 = X ∧ w ⁡ N − 2 ≠ w ⁡ 0